Add strictly positive numeric types

[riz0id]

proposing non-zero naturals and positive rationals and completing proofs for their properties with the algebraic morphism modules if necessary.

[MatthewDaggitt]

Hmm do you have a definition in mind? In practice due to the issue of converting backwards and forwards between them, it's often easier simply to enforce a non-zero requirement where needed. See Data.Nat.DivMod for an example of how to use implicit arguments to avoid having to pass the proof every time and see #921 for a proposed improvement.