Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)

This way, no more references to NBinDefs.N when doing "Print N".
Long-term migration to theories/Numbers is still planned, but it needs
more works, for instance to adapt both positive and N and Z at once.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10806 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 362 insertions, 284 deletions

diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 6c20107f3a..5d57c49dbb 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -96,7 +96,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
 (* Parsing N via scopes                                               *)
 (**********************************************************************)
 
-let binnat_module = ["Coq";"Numbers";"Natural";"Binary";"NBinDefs"]
+let binnat_module = ["Coq";"NArith";"BinNat"]
 let n_kn = make_kn (make_dir binnat_module) (id_of_string "N")
 let glob_n = IndRef (n_kn,0)
 let path_of_N0 = ((n_kn,0),1)
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 9949d612d0..b704f3d378 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -5,71 +5,194 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*                      Evgeny Makarov, INRIA, 2007                     *)
-(************************************************************************)
 
-(*i i*)
+(*i $Id$ i*)
 
 Require Import BinPos.
-Require Import NBinDefs.
+Unset Boxed Definitions.
+
+(**********************************************************************)
+(** Binary natural numbers *)
+
+Inductive N : Set :=
+  | N0 : N
+  | Npos : positive -> N.
 
-(*Unset Boxed Definitions.*)
+(** Declare binding key for scope positive_scope *)
 
 Delimit Scope N_scope with N.
+
+(** Automatically open scope positive_scope for the constructors of N *)
+
 Bind Scope N_scope with N.
+Arguments Scope Npos [positive_scope].
+
 Open Local Scope N_scope.
 
-(** Operations *)
-
-Notation N := N (only parsing).
-Notation N0 := N0 (only parsing).
-Notation Npos := Npos (only parsing).
-Notation Nsucc := succ (only parsing).
-Notation Npred := pred (only parsing).
-Notation Nplus := plus (only parsing).
-Notation Nminus := minus (only parsing).
-Notation Nmult := times (only parsing).
-Notation Ncompare := Ncompare (only parsing).
-Notation Nlt := lt (only parsing).
-Notation Nle := le (only parsing).
-Definition Ngt (x y : N) := (Ncompare x y) = Gt.
-Definition Nge (x y : N) := (Ncompare x y) <> Lt.
-Notation Nmin := min (only parsing).
-Notation Nmax := max (only parsing).
-
-(* If the notations for operations above had been actual definitions, the
-arguments scopes would have been N_scope due to the instruction "Bind Scope
-N_scope with N". However, the operations were declared in NBinary, where
-N_scope has not yet been declared. Therefore, we need to assign the
-arguments scopes manually. Note that this has to be done before declaring
-infix notations below. Ngt and Nge get their scope from the definition. *)
-
-Arguments Scope succ [N_scope].
-Arguments Scope pred [N_scope].
-Arguments Scope plus [N_scope N_scope].
-Arguments Scope minus [N_scope N_scope].
-Arguments Scope times [N_scope N_scope].
-Arguments Scope NBinDefs.Ncompare [N_scope N_scope].
-Arguments Scope lt [N_scope N_scope].
-Arguments Scope le [N_scope N_scope].
-Arguments Scope min [N_scope N_scope].
-Arguments Scope max [N_scope N_scope].
+Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }.
+Proof.
+ destruct n; auto.
+ left; exists p; auto.
+Defined.
+
+(** Operation x -> 2*x+1 *)
+
+Definition Ndouble_plus_one x :=
+  match x with
+  | N0 => Npos 1
+  | Npos p => Npos (xI p)
+  end.
+
+(** Operation x -> 2*x *)
+
+Definition Ndouble n := 
+  match n with
+  | N0 => N0
+  | Npos p => Npos (xO p)
+  end.
+
+(** Successor *)
+
+Definition Nsucc n :=
+  match n with
+  | N0 => Npos 1
+  | Npos p => Npos (Psucc p)
+  end.
+
+(** Predecessor *)
+
+Definition Npred (n : N) := match n with
+| N0 => N0
+| Npos p => match p with
+  | xH => N0
+  | _ => Npos (Ppred p)
+  end
+end.
+
+(** Addition *)
+
+Definition Nplus n m :=
+  match n, m with
+  | N0, _ => m
+  | _, N0 => n
+  | Npos p, Npos q => Npos (p + q)
+  end.
 
 Infix "+" := Nplus : N_scope.
+
+(** Subtraction *)
+
+Definition Nminus (n m : N) :=
+match n, m with
+| N0, _ => N0
+| n, N0 => n
+| Npos n', Npos m' =>
+  match Pminus_mask n' m' with
+  | IsPos p => Npos p
+  | _ => N0
+  end
+end.
+
 Infix "-" := Nminus : N_scope.
+
+(** Multiplication *)
+
+Definition Nmult n m :=
+  match n, m with
+  | N0, _ => N0
+  | _, N0 => N0
+  | Npos p, Npos q => Npos (p * q)
+  end.
+
 Infix "*" := Nmult : N_scope.
+
+(** Order *)
+
+Definition Ncompare n m :=
+  match n, m with
+  | N0, N0 => Eq
+  | N0, Npos m' => Lt
+  | Npos n', N0 => Gt
+  | Npos n', Npos m' => (n' ?= m')%positive Eq
+  end.
+
 Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
+
+Definition Nlt (x y:N) := (x ?= y) = Lt.
+Definition Ngt (x y:N) := (x ?= y) = Gt.
+Definition Nle (x y:N) := (x ?= y) <> Gt.
+Definition Nge (x y:N) := (x ?= y) <> Lt.
+
 Infix "<=" := Nle : N_scope.
 Infix "<" := Nlt : N_scope.
 Infix ">=" := Nge : N_scope.
 Infix ">" := Ngt : N_scope.
 
-(** Peano induction and recursion *)
+(** Min and max *)
+
+Definition Nmin (n n' : N) := match Ncompare n n' with 
+ | Lt | Eq => n
+ | Gt => n'
+ end.
+
+Definition Nmax (n n' : N) := match Ncompare n n' with 
+ | Lt | Eq => n'
+ | Gt => n
+ end.
+
+(** convenient induction principles *)
+
+Lemma N_ind_double :
+ forall (a:N) (P:N -> Prop),
+   P N0 ->
+   (forall a, P a -> P (Ndouble a)) ->
+   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
+Proof.
+  intros; elim a. trivial.
+  simple induction p. intros. 
+  apply (H1 (Npos p0)); trivial.
+  intros; apply (H0 (Npos p0)); trivial.
+  intros; apply (H1 N0); assumption.
+Qed.
+
+Lemma N_rec_double :
+ forall (a:N) (P:N -> Set),
+   P N0 ->
+   (forall a, P a -> P (Ndouble a)) ->
+   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
+Proof.
+  intros; elim a. trivial.
+  simple induction p. intros. 
+  apply (H1 (Npos p0)); trivial.
+  intros; apply (H0 (Npos p0)); trivial.
+  intros; apply (H1 N0); assumption.
+Qed.
+
+(** Peano induction on binary natural numbers *)
+
+Definition Nrect
+  (P : N -> Type) (a : P N0)
+    (f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n :=
+let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in
+let P' (p : positive) := P (Npos p) in
+match n return (P n) with
+| N0 => a
+| Npos p => Prect P' (f N0 a) f' p
+end.
+
+Theorem Nrect_base : forall P a f, Nrect P a f N0 = a.
+Proof.
+intros P a f; simpl; reflexivity.
+Qed.
+
+Theorem Nrect_step : forall P a f n, Nrect P a f (Nsucc n) = f n (Nrect P a f n).
+Proof.
+intros P a f; destruct n as [| p]; simpl;
+[rewrite Prect_base | rewrite Prect_succ]; reflexivity.
+Qed.
 
-Notation Nrect := Nrect (only parsing).
-Notation Nrect_base := Nrect_base (only parsing).
-Notation Nrect_step := Nrect_step (only parsing).
 Definition Nind (P : N -> Prop) := Nrect P.
+
 Definition Nrec (P : N -> Set) := Nrect P.
 
 Theorem Nrec_base : forall P a f, Nrec P a f N0 = a.
@@ -84,117 +207,214 @@ Qed.
 
 (** Properties of successor and predecessor *)
 
-Notation Npred_succ := pred_succ (only parsing).
-Notation Nsucc_0 := neq_succ_0 (only parsing).
-Notation Nsucc_inj := succ_inj (only parsing).
+Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n.
+Proof.
+destruct n as [| p]; simpl. reflexivity.
+case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ).
+intro H; false_hyp H Psucc_not_one.
+Qed.
 
 (** Properties of addition *)
 
-Notation Nplus_0_l := plus_0_l (only parsing).
-Notation Nplus_0_r := plus_0_r (only parsing).
-Notation Nplus_comm := plus_comm (only parsing).
-Notation Nplus_assoc := plus_assoc (only parsing).
-Notation Nplus_succ := plus_succ_l (only parsing).
-Notation Nplus_reg_l := (fun n m p : N => proj1 (plus_cancel_l m p n)) (only parsing).
+Theorem Nplus_0_l : forall n:N, N0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Theorem Nplus_0_r : forall n:N, n + N0 = n.
+Proof.
+destruct n; reflexivity.
+Qed.
+
+Theorem Nplus_comm : forall n m:N, n + m = m + n.
+Proof.
+intros.
+destruct n; destruct m; simpl in |- *; try reflexivity.
+rewrite Pplus_comm; reflexivity.
+Qed.
+
+Theorem Nplus_assoc : forall n m p:N, n + (m + p) = n + m + p.
+Proof.
+intros.
+destruct n; try reflexivity.
+destruct m; try reflexivity.
+destruct p; try reflexivity.
+simpl in |- *; rewrite Pplus_assoc; reflexivity.
+Qed.
+
+Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m).
+Proof.
+destruct n; destruct m.
+  simpl in |- *; reflexivity.
+  unfold Nsucc, Nplus in |- *; rewrite <- Pplus_one_succ_l; reflexivity.
+  simpl in |- *; reflexivity.
+  simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
+Qed.
+
+Theorem Nsucc_0 : forall n : N, Nsucc n <> N0.
+Proof.
+intro n; elim n; simpl Nsucc; intros; discriminate.
+Qed.
+
+Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m.
+Proof.
+destruct n; destruct m; simpl in |- *; intro H; reflexivity || injection H;
+ clear H; intro H.
+  symmetry  in H; contradiction Psucc_not_one with p.
+  contradiction Psucc_not_one with p.
+  rewrite Psucc_inj with (1 := H); reflexivity.
+Qed.
+
+Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p.
+Proof.
+intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *.
+  trivial.
+  intros n IHn m p H0; do 2 rewrite Nplus_succ in H0.
+  apply IHn; apply Nsucc_inj; assumption.
+Qed.
 
 (** Properties of subtraction. *)
 
-Notation Nminus_N0_Nle := minus_0_le (only parsing).
-Notation Nminus_0_r := minus_0_r (only parsing).
-Notation Nminus_succ_r := minus_succ_r (only parsing).
+Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'.
+Proof.
+destruct n as [| p]; destruct n' as [| q]; unfold Nle; simpl;
+split; intro H; try discriminate; try reflexivity.
+now elim H.
+intro H1; apply Pminus_mask_Gt in H1. destruct H1 as [h [H1 _]].
+rewrite H1 in H; discriminate.
+case_eq (Pcompare p q Eq); intro H1; rewrite H1 in H; try now elim H.
+assert (H2 : p = q); [now apply Pcompare_Eq_eq |]. now rewrite H2, Pminus_mask_diag.
+now rewrite Pminus_mask_Lt.
+Qed.
+
+Theorem Nminus_0_r : forall n : N, n - N0 = n.
+Proof.
+now destruct n.
+Qed.
+
+Theorem Nminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m).
+Proof.
+destruct n as [| p]; destruct m as [| q]; try reflexivity.
+now destruct p.
+simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
+now destruct (Pminus_mask p q) as [| r |]; [| destruct r |].
+Qed.
 
 (** Properties of multiplication *)
 
-Notation Nmult_0_l := times_0_l (only parsing).
-Notation Nmult_1_l := times_1_l (only parsing).
-Notation Nmult_1_r := times_1_r (only parsing).
-Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m.
+Theorem Nmult_0_l : forall n:N, N0 * n = N0.
 Proof.
-intros; now rewrite times_succ_l, Nplus_comm.
+reflexivity.
 Qed.
-Notation Nmult_comm := times_comm (only parsing).
-Notation Nmult_assoc := times_assoc (only parsing).
-Notation Nmult_plus_distr_r := times_plus_distr_r (only parsing).
-Notation Nmult_reg_r :=
-  (fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)) (only parsing).
 
-(** Properties of comparison *)
+Theorem Nmult_1_l : forall n:N, Npos 1 * n = n.
+Proof.
+destruct n; reflexivity.
+Qed.
 
-Notation Ncompare_Eq_eq := (fun n m : N => proj1 (Ncompare_eq_correct n m)) (only parsing).
-Notation Ncompare_refl := Ncompare_diag (only parsing).
-Notation Nlt_irrefl := lt_irrefl (only parsing).
+Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m.
+Proof.
+destruct n as [| n]; destruct m as [| m]; simpl; auto.
+rewrite Pmult_Sn_m; reflexivity.
+Qed.
 
-Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
+Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n.
 Proof.
-destruct n; destruct m; simpl; auto.
-exact (Pcompare_antisym p p0 Eq).
+destruct n; simpl in |- *; try reflexivity.
+rewrite Pmult_1_r; reflexivity.
 Qed.
 
-Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
+Theorem Nmult_comm : forall n m:N, n * m = m * n.
 Proof.
-destruct n; discriminate.
+intros.
+destruct n; destruct m; simpl in |- *; try reflexivity.
+rewrite Pmult_comm; reflexivity.
 Qed.
 
-(** Other properties and operations; given explicitly *)
+Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p.
+Proof.
+intros.
+destruct n; try reflexivity.
+destruct m; try reflexivity.
+destruct p; try reflexivity.
+simpl in |- *; rewrite Pmult_assoc; reflexivity.
+Qed.
 
-Definition Ndiscr : forall n : N, {p : positive | n = Npos p} + {n = N0}.
+Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p.
 Proof.
-destruct n; auto.
-left; exists p; auto.
-Defined.
+intros.
+destruct n; try reflexivity.
+destruct m; destruct p; try reflexivity.
+simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity.
+Qed.
 
-(** Operation x -> 2 * x + 1 *)
+Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m.
+Proof.
+destruct p; intros Hp H.
+contradiction Hp; reflexivity.
+destruct n; destruct m; reflexivity || (try discriminate H).
+injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity.
+Qed. 
 
-Definition Ndouble_plus_one x :=
-match x with
-| N0 => Npos 1
-| Npos p => Npos p~1
-end.
+(** Properties of comparison *)
 
-(** Operation x -> 2 * x *)
+Lemma Ncompare_refl : forall n, (n ?= n) = Eq.
+Proof.
+destruct n; simpl; auto.
+apply Pcompare_refl.
+Qed.
 
-Definition Ndouble n :=
-match n with
-| N0 => N0
-| Npos p => Npos p~0
-end.
+Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m.
+Proof.
+destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H;
+ reflexivity || (try discriminate H).
+  rewrite (Pcompare_Eq_eq n m H); reflexivity.
+Qed.
 
-(** convenient induction principles *)
+Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m.
+Proof.
+split; intros; 
+ [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ].
+Qed.
 
-Theorem N_ind_double :
- forall (a:N) (P:N -> Prop),
-   P N0 ->
-   (forall a, P a -> P (Ndouble a)) ->
-   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
+Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
 Proof.
-  intros; elim a. trivial.
-  simple induction p. intros.
-  apply (H1 (Npos p0)); trivial.
-  intros; apply (H0 (Npos p0)); trivial.
-  intros; apply (H1 N0); assumption.
+destruct n; destruct m; simpl; auto.
+exact (Pcompare_antisym p p0 Eq).
 Qed.
 
-Lemma N_rec_double :
- forall (a:N) (P:N -> Set),
-   P N0 ->
-   (forall a, P a -> P (Ndouble a)) ->
-   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
+Theorem Nlt_irrefl : forall n : N, ~ n < n.
 Proof.
-  intros; elim a. trivial.
-  simple induction p. intros.
-  apply (H1 (Npos p0)); trivial.
-  intros; apply (H0 (Npos p0)); trivial.
-  intros; apply (H1 N0); assumption.
+intro n; unfold Nlt; now rewrite Ncompare_refl.
 Qed.
 
-(** Division by 2 *)
+Theorem Ncompare_n_Sm :
+  forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m.
+Proof.
+intros n m; split; destruct n as [| p]; destruct m as [| q]; simpl; auto.
+destruct p; simpl; intros; discriminate.
+pose proof (proj1 (Pcompare_p_Sq p q));
+assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
+intros H; destruct H; discriminate.
+pose proof (proj2 (Pcompare_p_Sq p q));
+assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
+Qed.
+
+(** 0 is the least natural number *)
+
+Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
+Proof.
+destruct n; discriminate.
+Qed.
+
+(** Dividing by 2 *)
 
 Definition Ndiv2 (n:N) :=
   match n with
   | N0 => N0
   | Npos 1 => N0
-  | Npos p~0 => Npos p
-  | Npos p~1 => Npos p
+  | Npos (xO p) => Npos p
+  | Npos (xI p) => Npos p
   end.
 
 Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n.
@@ -218,4 +438,3 @@ Lemma Ndouble_plus_one_inj :
 Proof.
   intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2.
 Qed.
-
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index 66402f7614..3110da36a6 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -11,166 +11,25 @@
 (*i i*)
 
 Require Import BinPos.
+Require Export BinNat.
 Require Import NMinus.
 
-(** Definitions *)
+Open Local Scope N_scope.
 
-Inductive N : Set :=
-| N0 : N
-| Npos : positive -> N.
-
-Definition succ n :=
-match n with
-| N0 => Npos 1
-| Npos p => Npos (Psucc p)
-end.
-
-Definition pred (n : N) :=
-match n with
-| N0 => N0
-| Npos p =>
-  match p with
-  | xH => N0
-  | _ => Npos (Ppred p)
-  end
-end.
-
-Definition plus n m :=
-match n, m with
-| N0, _ => m
-| _, N0 => n
-| Npos p, Npos q => Npos (p + q)
-end.
-
-Definition minus (n m : N) :=
-match n, m with
-| N0, _ => N0
-| n, N0 => n
-| Npos n', Npos m' =>
-  match Pminus_mask n' m' with
-  | IsPos p => Npos p
-  | _ => N0
-  end
-end.
-
-Definition times n m :=
-match n, m with
-| N0, _ => N0
-| _, N0 => N0
-| Npos p, Npos q => Npos (p * q)
-end.
-
-Definition Ncompare n m :=
-match n, m with
-| N0, N0 => Eq
-| N0, Npos m' => Lt
-| Npos n', N0 => Gt
-| Npos n', Npos m' => (n' ?= m')%positive Eq
-end.
-
-Definition lt (x y : N) := (Ncompare x y) = Lt.
-Definition le (x y : N) := (Ncompare x y) <> Gt.
-
-Definition min (n m : N) :=
-match Ncompare n m with
-| Lt | Eq => n
-| Gt => m
-end.
-
-Definition max (n m : N) :=
-match Ncompare n m with
-| Lt | Eq => m
-| Gt => n
-end.
-
-Delimit Scope NatScope with Nat.
-Bind Scope NatScope with N.
-
-Notation "0" := N0 : NatScope.
-Notation "1" := (Npos xH) : NatScope.
-Infix "+" := plus : NatScope.
-Infix "-" := minus : NatScope.
-Infix "*" := times : NatScope.
-Infix "?=" := Ncompare (at level 70, no associativity) : NatScope.
-Infix "<" := lt : NatScope.
-Infix "<=" := le : NatScope.
-
-Open Local Scope NatScope.
-
-(** Peano induction on binary natural numbers *)
-
-Definition Nrect
-  (P : N -> Type) (a : P N0)
-    (f : forall n : N, P n -> P (succ n)) (n : N) : P n :=
-let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in
-let P' (p : positive) := P (Npos p) in
-match n return (P n) with
-| N0 => a
-| Npos p => Prect P' (f N0 a) f' p
-end.
-
-Theorem Nrect_base : forall P a f, Nrect P a f N0 = a.
-Proof.
-reflexivity.
-Qed.
-
-Theorem Nrect_step : forall P a f n, Nrect P a f (succ n) = f n (Nrect P a f n).
-Proof.
-intros P a f; destruct n as [| p]; simpl;
-[rewrite Prect_base | rewrite Prect_succ]; reflexivity.
-Qed.
-
-(*Definition Nind (P : N -> Prop) := Nrect P.
-
-Definition Nrec (P : N -> Set) := Nrect P.
-
-Theorem Nrec_base : forall P a f, Nrec P a f N0 = a.
-Proof.
-intros P a f; unfold Nrec; apply Nrect_base.
-Qed.
-
-Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n).
-Proof.
-intros P a f; unfold Nrec; apply Nrect_step.
-Qed.*)
-
-(** Results about the order *)
-
-Theorem Ncompare_eq_correct : forall n m : N, (n ?= m) = Eq <-> n = m.
-Proof.
-destruct n as [| n]; destruct m as [| m]; simpl;
-split; intro H; try reflexivity; try discriminate H.
-apply Pcompare_Eq_eq in H; now rewrite H.
-injection H; intro H1; rewrite H1; apply Pcompare_refl.
-Qed.
-
-Theorem Ncompare_diag : forall n : N, n ?= n = Eq.
-Proof.
-intro n; now apply <- Ncompare_eq_correct.
-Qed.
-
-Theorem Ncompare_antisymm :
-  forall (n m : N) (c : comparison), n ?= m = c -> m ?= n = CompOpp c.
-Proof.
-destruct n; destruct m; destruct c; simpl; intro H; try discriminate H; try reflexivity;
-replace Eq with (CompOpp Eq) by reflexivity; rewrite <- Pcompare_antisym;
-now rewrite H.
-Qed.
-
-(** Implementation of NAxiomsSig module type *)
+(** Implementation of [NAxiomsSig] module type via [BinNat.N] *)
 
 Module NBinaryAxiomsMod <: NAxiomsSig.
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
 
 Definition NZ := N.
-Definition NZeq := (@eq N).
+Definition NZeq := @eq N.
 Definition NZ0 := N0.
-Definition NZsucc := succ.
-Definition NZpred := pred.
-Definition NZplus := plus.
-Definition NZminus := minus.
-Definition NZtimes := times.
+Definition NZsucc := Nsucc.
+Definition NZpred := Npred.
+Definition NZplus := Nplus.
+Definition NZminus := Nminus.
+Definition NZtimes := Nmult.
 
 Theorem NZeq_equiv : equiv N NZeq.
 Proof (eq_equiv N).
@@ -229,7 +88,7 @@ Theorem NZplus_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m).
 Proof.
 destruct n; destruct m.
 simpl in |- *; reflexivity.
-unfold NZsucc, NZplus, succ, plus. rewrite <- Pplus_one_succ_l; reflexivity.
+unfold NZsucc, NZplus, Nsucc, Nplus. rewrite <- Pplus_one_succ_l; reflexivity.
 simpl in |- *; reflexivity.
 simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
 Qed.
@@ -260,10 +119,10 @@ Qed.
 
 End NZAxiomsMod.
 
-Definition NZlt := lt.
-Definition NZle := le.
-Definition NZmin := min.
-Definition NZmax := max.
+Definition NZlt := Nlt.
+Definition NZle := Nle.
+Definition NZmin := Nmin.
+Definition NZmax := Nmax.
 
 Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
 Proof.
@@ -287,19 +146,19 @@ Qed.
 
 Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m.
 Proof.
-intros n m. unfold le, lt. rewrite <- Ncompare_eq_correct.
+intros n m. unfold Nle, Nlt. rewrite <- Ncompare_eq_correct.
 destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now right.
 now elim H1. destruct H1; discriminate.
 Qed.
 
 Theorem NZlt_irrefl : forall n : NZ, ~ n < n.
 Proof.
-intro n; unfold lt; now rewrite Ncompare_diag.
+intro n; unfold Nlt; now rewrite Ncompare_refl.
 Qed.
 
 Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m.
 Proof.
-intros n m; unfold lt, le; destruct n as [| p]; destruct m as [| q]; simpl;
+intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl;
 split; intro H; try reflexivity; try discriminate.
 destruct p; simpl; intros; discriminate. elimtype False; now apply H.
 apply -> Pcompare_p_Sq in H. destruct H as [H | H].
@@ -310,29 +169,29 @@ Qed.
 
 Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n.
 Proof.
-unfold NZmin, min, le; intros n m H.
+unfold NZmin, Nmin, Nle; intros n m H.
 destruct (n ?= m); try reflexivity. now elim H.
 Qed.
 
 Theorem NZmin_r : forall n m : N, m <= n -> NZmin n m = m.
 Proof.
-unfold NZmin, min, le; intros n m H.
+unfold NZmin, Nmin, Nle; intros n m H.
 case_eq (n ?= m); intro H1; try reflexivity.
 now apply -> Ncompare_eq_correct.
-apply Ncompare_antisymm in H1. now elim H.
+rewrite <- Ncompare_antisym, H1 in H; elim H; auto.
 Qed.
 
 Theorem NZmax_l : forall n m : N, m <= n -> NZmax n m = n.
 Proof.
-unfold NZmax, max, le; intros n m H.
+unfold NZmax, Nmax, Nle; intros n m H.
 case_eq (n ?= m); intro H1; try reflexivity.
 symmetry; now apply -> Ncompare_eq_correct.
-apply Ncompare_antisymm in H1. now elim H.
+rewrite <- Ncompare_antisym, H1 in H; elim H; auto.
 Qed.
 
 Theorem NZmax_r : forall n m : N, n <= m -> NZmax n m = m.
 Proof.
-unfold NZmax, max, le; intros n m H.
+unfold NZmax, Nmax, Nle; intros n m H.
 destruct (n ?= m); try reflexivity. now elim H.
 Qed.
 
@@ -342,7 +201,7 @@ Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
   Nrect (fun _ => A) a f n.
 Implicit Arguments recursion [A].
 
-Theorem pred_0 : pred N0 = N0.
+Theorem pred_0 : Npred N0 = N0.
 Proof.
 reflexivity.
 Qed.
@@ -373,7 +232,7 @@ Qed.
 Theorem recursion_succ :
   forall (A : Set) (Aeq : relation A) (a : A) (f : N -> A -> A),
     Aeq a a -> fun2_wd NZeq Aeq Aeq f ->
-      forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
+      forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)).
 Proof.
 unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect.
 rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.