[ fix ] Outstanding issues with existing `Tactic.*Solver` and `Algebra.Solver.*` implementations

[jamesmckinna]

This is a portmanteau issue trying to bring together (and record successful solutions to!?):

• Replace Tactic.RingSolver.Core.NatSet with Data.Tree.AVL #1068
• Deprecate Algebra.Solver.Ring in favour of Tactic.RingSolver #1069
• Problem with exponentiation in Data.Nat.Tactic.RingSolver #1070
• Ring solver doesn't appear to normalise terms? #1071
• Tactic.RingSolver doesn't work over generic rings #1116
• Literals for any ring? #1363 in as much as Polynomial expressions over an ACR deserve to be able to use Nat literals
• Algebra.Solver.Ring allows us to specify a coefficient ring, but not here #2700
• Problem with Tactic.MonoidSolver #2710

with #459 as the inciting incident (which didn't seem to be closed by #800 #922 ?) in the hope of finally being able to close that one ;-)

Related: #2702 (and perhaps also #2457 ...)

Please add others and/or note other issues here if you come across them!