diff options
| -rw-r--r-- | theories/NArith/BinNat.v | 35 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 2 |
2 files changed, 36 insertions, 1 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index fcd90c3aea..a1a12017ab 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -521,3 +521,38 @@ Proof. now rewrite Nmult_1_r. apply Piter_op_succ. apply Nmult_assoc. Qed. + +(** Parity *) + +Definition Neven n := + match n with + | N0 => true + | Npos (xO _) => true + | _ => false + end. +Definition Nodd n := negb (Neven n). + +Local Notation "1" := (Npos xH) : N_scope. +Local Notation "2" := (Npos (xO xH)) : N_scope. + +Lemma Neven_spec : forall n, Neven n = true <-> exists m, n=2*m. +Proof. + destruct n. + split. now exists N0. + trivial. + destruct p; simpl; split; trivial; try discriminate. + intros (m,H). now destruct m. + now exists (Npos p). + intros (m,H). now destruct m. +Qed. + +Lemma Nodd_spec : forall n, Nodd n = true <-> exists m, n=2*m+1. +Proof. + destruct n. + split. discriminate. + intros (m,H). now destruct m. + destruct p; simpl; split; trivial; try discriminate. + exists (Npos p). reflexivity. + intros (m,H). now destruct m. + exists N0. reflexivity. +Qed. diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 61d88af5c1..1ba3f2992e 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -20,7 +20,7 @@ Module N. Include NBinary.N. End N. -(** [N] contains An [order] tactic for natural numbers *) +(** [N] contains an [order] tactic for natural numbers *) (** Note that [N.order] is domain-agnostic: it will not prove [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) |