Tidy up the interfaces between modules

[Smaug123]

For example, the functions in Naturals.agda leak out and are used pretty extensively in Integers.agda. We'd prefer to be stricter about accessing these functions in a canonical way through the appropriate group structure or whatever. A good example of this being done properly is with Orders: most uses of orders are through the well-known functions PartialOrder.irreflexive and friends, rather than specific functions like aLessA (which specifically works on the naturals only).

[Smaug123]

This is happening slowly; need to try and remove references to things which aren't Numbers.Naturals.Naturals, for example, since that module hides many of the internals of the Numbers.Naturals namespace.