# Library Coq.Numbers.Natural.Abstract.NParity

Require Import Bool NSub NZParity.
Some additionnal properties of even, odd.
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.