Extra rules about prime fields.
These are candidate for inclusion in the prime fields library. They are in the elliptic curve library right now because they are used in proofs about elliptic curves, but they are general.
It may be possible to simplify some of the proofs, with better us of the exising prime field rules.
These extra rules may also need to be examined in relation to the intended normal forms of the existing prime field rules.