Library Coq.Numbers.Natural.Abstract.NParity

Require Import Bool NSub NZParity.

Module Type NParityProp (Import N : NAxiomsSig´)(Import NP : NSubProp N).

Include NZParityProp N N NP.

Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n.

Lemma even_pred : forall n, n~=0 -> even (P n) = odd n.

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

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

End NParityProp.