Add tactic-style ring solvers for rational and unnormalised rational numbers

[dancewithheart]

This updates the old rational ring-solver work to current stdlib.

The base solver modules already exist (Data.Rational.Solver and
Data.Rational.Unnormalised.Solver); this PR

• adds tactic-style wrappers analogous to Data.Nat.Tactic.RingSolver,
• factors the weak zero recognizers into the corresponding Properties modules (that was suggested in review for 2215),
• adds README examples.

For normalized rationals the tactic wrapper targets propositional equality
≡, while for unnormalised rationals it targets rational equivalence ≃.

This PR continues/supersedes #2215, which I opened from my old GitHub account.

Fixes #1879.

[dancewithheart]

Tested locally with:

agda -i src -i . src/Data/Rational/Properties.agda
agda -i src -i . src/Data/Rational/Tactic/RingSolver.agda

agda -i src -i . src/Data/Rational/Unnormalised/Properties.agda 
agda -i src -i . src/Data/Rational/Unnormalised/Tactic/RingSolver.agda

cd doc
agda -i ../src -i . README/Data/Rational.agda
agda -i ../src -i . README/Data/Rational/Unnormalised.agda

make test