Small refactorings for elementary number theory

[fredrik-bakke]

The elementary-number-theory module is in need of some love and attention. This issue is not aiming for a complete overhaul as one might be tempted to, but I will record some select glaring issues that should be easier to resolve.

This issue is a work in progress

Elementary number theory

• [ ] Factor strict inequality into their own files separate from inequality
• [ ] Decide on whether to go for the formulation preserves-strict-order or preserves-le
• [ ] Factor out positive and negative integers into a separate module(s).
• [ ] Define the expected implications: strict inequality implies inequality
• [ ] Define the expected entries where decidability is claimed.