Library Coq.Numbers.Integer.Abstract.ZParity

Require Import Bool ZMulOrder NZParity.

Module Type ZParityProp (Import Z : ZAxiomsSig´)
                        (Import ZP : ZMulOrderProp Z).

Include NZParityProp Z Z ZP.

Lemma odd_pred : forall n, odd (P n) = even n.

Lemma even_pred : forall n, even (P n) = odd n.

Lemma even_opp : forall n, even (-n) = even n.

Lemma odd_opp : forall n, odd (-n) = odd n.

Lemma even_sub : forall n m, even (n-m) = Bool.eqb (even n) (even m).

Lemma odd_sub : forall n m, odd (n-m) = xorb (odd n) (odd m).

End ZParityProp.