Remove uses of `Data.Nat.Solver` from a number of places

[JacquesCarette]

Various places gratuitously used Data.Nat.Solver when some fairly simple direct proofs could be used instead. This made Data.Rational (amongst others) very 'high' on the dependency graph when this was not needed.

[Taneb]

Various places gratuitously used Data.Nat.Solver when some fairly simple direct proofs could be used instead.

Having looked at the changes, I'm not sure if some of these can be called "simple". I wonder if a parallel effort might be to reduce the dependency foot print of the solvers instead? Fundamentally the solvers should use be able to use the boolean decision procedures in the Base modules rather than Dec decision procedures in Properties right?

You'd still need all the algebra laws, which still brings in .Properties...

[MatthewDaggitt]

You'd still need all the algebra laws, which still brings in .Properties...

Hmm good point!

[JacquesCarette]

Having looked at the changes, I'm not sure if some of these can be called "simple".

Compared to a lot of proofs in agda-categories, they are... but point taken. Though I'd say that many of them are no worse than some of the monsters in the same files. (Data.Integer.Properties is seriously frightening; I'll open some issues later.)

[JacquesCarette]

(Normally don't merge my own, but I take the above as permission to do so rather than waiting.)