Replaced BinNat with a new version that is based on theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers.

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

34 files changed, 1235 insertions, 641 deletions

diff --git a/Makefile.common b/Makefile.common
index 47102d69f..eb6639ea7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -670,7 +670,11 @@ NATURALABSTRACTVO:=\
   $(NATABSTRACTDIR)/NIso.vo
 
 NATURALPEANOVO:=$(NATURALDIR)/Peano/NPeano.vo
-NATURALBINARYVO:=$(NATURALDIR)/Binary/NBinary.vo
+
+NATURALBINARYVO:=\
+  $(NATURALDIR)/Binary/NBinDefs.vo
+  $(NATURALDIR)/Binary/NBinary.vo
+
 NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO)
 
 INTEGERDIR:=$(NUMBERSDIR)/Integer
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index fd3802446..fd5fa1f69 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -443,7 +443,7 @@ Add Morphism (pow_pos rmul) : pow_morph.
 intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH].
 Qed.
 
-Add Morphism (pow_N rI rmul) : pow_N_morph.
+Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph.
 intros x y H [|p];simpl;auto. apply pow_morph;trivial.
 Qed.
 (*
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 5d57c49db..6c20107f3 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";"NArith";"BinNat"]
+let binnat_module = ["Coq";"Numbers";"Natural";"Binary";"NBinDefs"]
 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 96083891b..349892b99 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -5,205 +5,71 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
 
-(*i $Id$ i*)
+(*i i*)
 
 Require Import BinPos.
-Unset Boxed Definitions.
-
-(**********************************************************************)
-(** Binary natural numbers *)
-
-Inductive N : Set :=
-  | N0 : N
-  | Npos : positive -> N.
+Require Import NBinDefs.
 
-(** Declare binding key for scope positive_scope *)
+(*Unset Boxed Definitions.*)
 
 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.
 
-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.
+(** Operations *)
+
+Notation N := N.
+Notation N0 := N0.
+Notation Npos := Npos.
+Notation Nsucc := succ.
+Notation Npred := pred.
+Notation Nplus := plus.
+Notation Nminus := minus.
+Notation Nmult := times.
+Notation Ncompare := Ncompare.
+Notation Nlt := lt.
+Notation Nle := le.
+Definition Ngt (x y : N) := (Ncompare x y) = Gt.
+Definition Nge (x y : N) := (Ncompare x y) <> Lt.
+Notation Nmin := min.
+Notation Nmax := max.
+
+(* 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].
 
 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.
-
-(*Definition Nminus (x y:N) :=
-  match x, y with
-    | N0, _ => N0
-    | x, N0 => x
-    | Npos x', Npos y' =>
-      match Pcompare x' y' Eq with
-        | Lt | Eq => N0
-        | Gt => Npos (x' - y')
-      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.
 
-(** 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.
+(** Peano induction and recursion *)
 
+Notation Nrect := Nrect.
+Notation Nrect_base := Nrect_base.
+Notation Nrect_step := Nrect_step.
 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.
@@ -218,201 +84,111 @@ Qed.
 
 (** Properties of successor and predecessor *)
 
-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.
+Notation Npred_succ := pred_succ.
+Notation Nsucc_0 := neq_succ_0.
+Notation Nsucc_inj := succ_inj.
 
 (** Properties of addition *)
 
-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.
+Notation Nplus_0_l := plus_0_l.
+Notation Nplus_0_r := plus_0_r.
+Notation Nplus_comm := plus_comm.
+Notation Nplus_assoc := plus_assoc.
+Notation Nplus_succ := plus_succ_l.
+Notation Nplus_reg_l := (fun n m p : N => proj1 (plus_cancel_l m p n)).
 
 (** Properties of subtraction. *)
 
-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.
+Notation Nminus_N0_Nle :=
+  (fun n m : N => (conj (proj2 (le_minus_0 n m)) (proj1 (le_minus_0 n m)))).
+Notation Nminus_0_r := minus_0_r.
+Notation Nminus_succ_r := minus_succ_r.
 
 (** Properties of multiplication *)
 
-Theorem Nmult_0_l : forall n:N, N0 * n = N0.
-Proof.
-reflexivity.
-Qed.
-
-Theorem Nmult_1_l : forall n:N, Npos 1 * n = n.
-Proof.
-destruct n; reflexivity.
-Qed.
-
+Notation Nmult_0_l := times_0_l.
+Notation Nmult_1_l := times_1_l.
+Notation Nmult_1_r := times_1_r.
 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.
+intros; now rewrite times_succ_l, Nplus_comm.
 Qed.
+Notation Nmult_comm := times_comm.
+Notation Nmult_assoc := times_assoc.
+Notation Nmult_plus_distr_r := times_plus_distr_r.
+Notation Nmult_reg_r :=
+  (fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)).
 
-Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n.
-Proof.
-destruct n; simpl in |- *; try reflexivity.
-rewrite Pmult_1_r; reflexivity.
-Qed.
+(** Properties of comparison *)
 
-Theorem Nmult_comm : forall n m:N, n * m = m * n.
-Proof.
-intros.
-destruct n; destruct m; simpl in |- *; try reflexivity.
-rewrite Pmult_comm; reflexivity.
-Qed.
+Notation Ncompare_Eq_eq := (fun n m : N => proj1 (Ncompare_eq_correct n m)).
+Notation Ncompare_refl := Ncompare_diag.
+Notation Nlt_irrefl := lt_irrefl.
 
-Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p.
+Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
 Proof.
-intros.
-destruct n; try reflexivity.
-destruct m; try reflexivity.
-destruct p; try reflexivity.
-simpl in |- *; rewrite Pmult_assoc; reflexivity.
+destruct n; destruct m; simpl; auto.
+exact (Pcompare_antisym p p0 Eq).
 Qed.
 
-Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p.
+Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
 Proof.
-intros.
-destruct n; try reflexivity.
-destruct m; destruct p; try reflexivity.
-simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity.
+destruct n; discriminate.
 Qed.
 
-Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m.
+(** Other properties and operations; given explicitly *)
+
+Definition Ndiscr : forall n : N, {p : positive | n = Npos p} + {n = N0}.
 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. 
+destruct n; auto.
+left; exists p; auto.
+Defined.
 
-(** Properties of comparison *)
+(** Operation x -> 2 * x + 1 *)
 
-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.
+Definition Ndouble_plus_one x :=
+match x with
+| N0 => Npos 1
+| Npos p => Npos (xI p)
+end.
 
-Lemma Ncompare_refl : forall n, (n ?= n) = Eq.
-Proof.
-destruct n; simpl; auto.
-apply Pcompare_refl.
-Qed.
+(** Operation x -> 2 * x *)
 
-Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
-Proof.
-destruct n; destruct m; simpl; auto.
-exact (Pcompare_antisym p p0 Eq).
-Qed.
+Definition Ndouble n :=
+match n with
+| N0 => N0
+| Npos p => Npos (xO p)
+end.
 
-Theorem Nlt_irrefl : forall n : N, ~ n < n.
-Proof.
-intro n; unfold Nlt; now rewrite Ncompare_refl.
-Qed.
+(** convenient induction principles *)
 
-Theorem Ncompare_n_Sm :
-  forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m.
+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.
 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].
+  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.
 
-(** 0 is the least natural number *)
-
-Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
+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.
-destruct n; discriminate.
+  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.
 
-(** Dividing by 2 *)
+(** Division by 2 *)
 
 Definition Ndiv2 (n:N) :=
   match n with
@@ -443,3 +219,4 @@ 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/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 0e47356ad..e81cffe4f 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NZAxioms.
 
 Set Implicit Arguments.
@@ -15,6 +27,10 @@ Notation P := NZpred.
 Notation Zplus := NZplus.
 Notation Ztimes := NZtimes.
 Notation Zminus := NZminus.
+Notation Zlt := NZlt.
+Notation Zle := NZle.
+Notation Zmin := NZmin.
+Notation Zmax := NZmax.
 Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
 Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 Notation "0" := NZ0 : IntScope.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index dbe2aa439..ace49428d 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZAxioms.
 Require Import NZTimesOrder.
 
@@ -7,6 +19,12 @@ Open Local Scope IntScope.
 
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
+Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2.
+Proof NZsucc_wd.
+
+Theorem Zpred_wd : forall n1 n2 : Z, n1 == n2 -> P n1 == P n2.
+Proof NZpred_wd.
+
 Theorem Zpred_succ : forall n : Z, P (S n) == n.
 Proof NZpred_succ.
 
@@ -22,6 +40,15 @@ Proof NZsucc_inj_wd.
 Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
+(* Decidability and stability of equality was proved only in NZOrder, but
+since it does not mention order, we'll put it here *)
+
+Theorem Zeq_em : forall n m : Z, n == m \/ n ~= m.
+Proof NZeq_em.
+
+Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
+Proof NZeq_dne.
+
 Theorem Zcentral_induction :
 forall A : Z -> Prop, predicate_wd Zeq A ->
   forall z : Z, A z ->
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 3146b9c2c..51b522a52 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NumPrelude.
 
 Module Type ZDomainSignature.
@@ -6,14 +18,14 @@ Parameter Inline Z : Set.
 Parameter Inline Zeq : Z -> Z -> Prop.
 Parameter Inline e : Z -> Z -> bool.
 
-Axiom E_equiv_e : forall x y : Z, Zeq x y <-> e x y.
-Axiom E_equiv : equiv Z Zeq.
+Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y.
+Axiom eq_equiv : equiv Z Zeq.
 
 Add Relation Z Zeq
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
+ reflexivity proved by (proj1 eq_equiv)
+ symmetry proved by (proj2 (proj2 eq_equiv))
+ transitivity proved by (proj1 (proj2 eq_equiv))
+as eq_rel.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
@@ -29,12 +41,12 @@ Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
 Proof.
 intros x x' Exx' y y' Eyy'.
 case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
-assert (x == y); [apply <- E_equiv_e; now rewrite H2 |
+assert (x == y); [apply <- eq_equiv_e; now rewrite H2 |
 assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
-rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]].
-assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 |
+rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]].
+assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 |
 assert (x == y); [rewrite Exx'; now rewrite Eyy' |
-rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
+rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
 Qed.
 
 Theorem neq_symm : forall n m, n # m -> m # n.
@@ -50,7 +62,7 @@ Qed.
 Declare Left Step ZE_stepl.
 
 (* The right step lemma is just transitivity of Zeq *)
-Declare Right Step (proj1 (proj2 E_equiv)).
+Declare Right Step (proj1 (proj2 eq_equiv)).
 
 End ZDomainProperties.
 
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index 322d36cd3..9b452039c 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZTimes.
 
 Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
@@ -6,6 +18,22 @@ Open Local Scope IntScope.
 
 (* Axioms *)
 
+Theorem Zlt_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2).
+Proof NZlt_wd.
+
+Theorem Zle_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
+Proof NZle_wd.
+
+Theorem Zmin_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2.
+Proof NZmin_wd.
+
+Theorem Zmax_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
+Proof NZmax_wd.
+
 Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
 Proof NZle_lt_or_eq.
 
@@ -15,6 +43,18 @@ Proof NZlt_irrefl.
 Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m.
 Proof NZlt_succ_le.
 
+Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
+Proof NZmin_l.
+
+Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m.
+Proof NZmin_r.
+
+Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n.
+Proof NZmax_l.
+
+Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m.
+Proof NZmax_r.
+
 (* Renaming theorems from NZOrder.v *)
 
 Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
@@ -91,12 +131,18 @@ Proof NZle_antisymm.
 Theorem Zlt_trichotomy : forall n m : Z,  n < m \/ n == m \/ m < n.
 Proof NZlt_trichotomy.
 
+Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
+Proof NZlt_gt_cases.
+
 Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
 Proof NZle_gt_cases.
 
 Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
 Proof NZlt_ge_cases.
 
+Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m.
+Proof NZle_ge_cases.
+
 Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
 Proof NZle_ngt.
 
@@ -164,9 +210,9 @@ Proof NZright_induction'.
 Theorem Zleft_induction' :
   forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z,
-    (forall n : NZ, z <= n -> A n) ->
+    (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
-      forall n : NZ, A n.
+      forall n : Z, A n.
 Proof NZleft_induction'.
 
 Theorem Zstrong_right_induction :
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index bae74feca..16fe11431 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -1,9 +1,25 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZBase.
 
 Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
+Theorem Zplus_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2.
+Proof NZplus_wd.
+
 Theorem Zplus_0_l : forall n : Z, 0 + n == n.
 Proof NZplus_0_l.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 49fd6f558..01226b121 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZOrder.
 
 Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 0290c237b..14c59fcfa 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export Ring.
 Require Export ZPlus.
 
@@ -5,6 +17,10 @@ Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
+Theorem Ztimes_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2.
+Proof NZtimes_wd.
+
 Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
 Proof NZtimes_0_r.
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index b1a0551f8..1b9e9b519 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZPlusOrder.
 
 Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
@@ -37,6 +49,9 @@ Proof NZtimes_le_mono_nonpos_r.
 Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof NZtimes_cancel_l.
 
+Theorem Ztimes_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
+Proof NZtimes_cancel_r.
+
 Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof NZtimes_le_mono_pos_l.
 
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 85596562e..3c680ec91 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import ZTimesOrder.
 Require Import ZArith.
 
@@ -16,16 +28,16 @@ Definition NZplus := Zplus.
 Definition NZminus := Zminus.
 Definition NZtimes := Zmult.
 
-Theorem NZE_equiv : equiv Z NZeq.
+Theorem NZeq_equiv : equiv Z NZeq.
 Proof.
 exact (@eq_equiv Z).
 Qed.
 
 Add Relation Z NZeq
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+as NZeq_rel.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
@@ -102,6 +114,8 @@ End NZAxiomsMod.
 
 Definition NZlt := Zlt.
 Definition NZle := Zle.
+Definition NZmin := Zmin.
+Definition NZmax := Zmax.
 
 Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
 Proof.
@@ -113,6 +127,16 @@ Proof.
 unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
 Qed.
 
+Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
+Proof.
+congruence.
+Qed.
+
 Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n = m.
 Proof.
 intros n m; split. apply Zle_lt_or_eq.
@@ -130,6 +154,34 @@ intros; unfold NZsucc; rewrite <- Zsucc_succ'; split;
 [apply Zlt_succ_le | apply Zle_lt_succ].
 Qed.
 
+Theorem NZmin_l : forall n m : NZ, n <= m -> NZmin n m = n.
+Proof.
+unfold NZmin, Zmin, Zle; intros n m H.
+destruct (n ?= m); try reflexivity. now elim H.
+Qed.
+
+Theorem NZmin_r : forall n m : NZ, m <= n -> NZmin n m = m.
+Proof.
+unfold NZmin, Zmin, Zle; intros n m H.
+case_eq (n ?= m); intro H1; try reflexivity.
+now apply Zcompare_Eq_eq.
+apply <- Zcompare_Gt_Lt_antisym in H1. now elim H.
+Qed.
+
+Theorem NZmax_l : forall n m : NZ, m <= n -> NZmax n m = n.
+Proof.
+unfold NZmax, Zmax, Zle; intros n m H.
+case_eq (n ?= m); intro H1; try reflexivity.
+apply <- Zcompare_Gt_Lt_antisym in H1. now elim H.
+Qed.
+
+Theorem NZmax_r : forall n m : NZ, n <= m -> NZmax n m = m.
+Proof.
+unfold NZmax, Zmax, Zle; intros n m H.
+case_eq (n ?= m); intro H1.
+now apply Zcompare_Eq_eq. reflexivity. now elim H.
+Qed.
+
 End NZOrdAxiomsMod.
 
 Definition Zopp (x : Z) :=
@@ -167,7 +219,7 @@ Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod.
 
 
 (*
-Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
+Theorem eq_equiv_e : forall x y : Z, E x y <-> e x y.
 Proof.
 intros x y; unfold E, e, Zeq_bool; split; intro H.
 rewrite H; now rewrite Zcompare_refl.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 38e8e097a..8e31331b4 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,26 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import NMinus. (* The most complete file for natural numbers *)
 Require Export ZTimesOrder. (* The most complete file for integers *)
 
 Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
 Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
 
+(* We do not declare ring in Natural/Abstract for two reasons. First, some
+of the properties proved in NPlus and NTimes are used in the new BinNat,
+and it is in turn used in Ring. Using ring in Natural/Abstract would be
+circular. It is possible, however, not to make BinNat dependent on
+Numbers/Natural and prove the properties necessary for ring from scratch
+(this is, of course, how it used to be). In addition, if we define semiring
+structures in the implementation subdirectories of Natural, we are able to
+specify binary natural numbers as the type of coefficients. For these
+reasons we define an abstract semiring here. *)
+
+Open Local Scope NatScope.
+
+Lemma Nsemi_ring : semi_ring_theory 0 1 plus times Neq.
+Proof.
+constructor.
+exact plus_0_l.
+exact plus_comm.
+exact plus_assoc.
+exact times_1_l.
+exact times_0_l.
+exact times_comm.
+exact times_assoc.
+exact times_plus_distr_r.
+Qed.
+
+Add Ring NSR : Nsemi_ring.
+
 (* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by
 the properties functor. Since we don't want Zplus_comm to refer to unfolded
 definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
 we will provide an extra layer of definitions. *)
 
-Open Local Scope NatIntScope.
 Definition Z := (N * N)%type.
 Definition Z0 : Z := (0, 0).
 Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
 Definition Zsucc (n : Z) : Z := (S (fst n), snd n).
 Definition Zpred (n : Z) : Z := (fst n, S (snd n)).
 
-(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) = n. It
+(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) == n. It
 could be possible to consider as canonical only pairs where one of the
 elements is 0, and make all operations convert canonical values into other
-canonical values. In that case, we could get rid of setoids as well as
-arrive at integers as signed natural numbers. *)
+canonical values. In that case, we could get rid of setoids and arrive at
+integers as signed natural numbers. *)
 
 Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
 Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
@@ -32,6 +70,8 @@ Definition Ztimes (n m : Z) : Z :=
   ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
 Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
 Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
+Definition Zmin (n m : Z) := (min ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).
+Definition Zmax (n m : Z) := (max ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
@@ -84,16 +124,16 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
 now apply -> plus_cancel_r in H3.
 Qed.
 
-Theorem NZE_equiv : equiv Z Zeq.
+Theorem NZeq_equiv : equiv Z Zeq.
 Proof.
 unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
 Qed.
 
 Add Relation Z Zeq
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+as NZeq_rel.
 
 Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
 Proof.
@@ -152,7 +192,7 @@ ring.
 Qed.
 
 Section Induction.
-Open Scope NatIntScope. (* automatically closes at the end of the section *)
+Open Scope NatScope. (* automatically closes at the end of the section *)
 Variable A : Z -> Prop.
 Hypothesis A_wd : predicate_wd Zeq A.
 
@@ -227,6 +267,8 @@ End NZAxiomsMod.
 
 Definition NZlt := Zlt.
 Definition NZle := Zle.
+Definition NZmin := Zmin.
+Definition NZmax := Zmax.
 
 Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
 Proof.
@@ -255,6 +297,38 @@ fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%I
 now rewrite H1, H2.
 Qed.
 
+Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.
+Proof.
+intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl.
+destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
+rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
+rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)).
+now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
+stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
+unfold Zeq in H1. rewrite H1. ring.
+rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
+rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)).
+now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
+stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
+unfold Zeq in H2. rewrite H2. ring.
+Qed.
+
+Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.
+Proof.
+intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl.
+destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
+rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
+rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)).
+now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
+stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
+unfold Zeq in H2. rewrite H2. ring.
+rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
+rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)).
+now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
+stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
+unfold Zeq in H1. rewrite H1. ring.
+Qed.
+
 Open Local Scope IntScope.
 
 Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
@@ -272,6 +346,30 @@ Proof.
 intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_le.
 Qed.
 
+Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
+Proof.
+unfold Zmin, Zle, Zeq; simpl; intros n m H.
+rewrite min_l. assumption. ring.
+Qed.
+
+Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m.
+Proof.
+unfold Zmin, Zle, Zeq; simpl; intros n m H.
+rewrite min_r. assumption. ring.
+Qed.
+
+Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n.
+Proof.
+unfold Zmax, Zle, Zeq; simpl; intros n m H.
+rewrite max_l. assumption. ring.
+Qed.
+
+Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m.
+Proof.
+unfold Zmax, Zle, Zeq; simpl; intros n m H.
+rewrite max_r. assumption. ring.
+Qed.
+
 End NZOrdAxiomsMod.
 
 Definition Zopp (n : Z) : Z := (snd n, fst n).
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index 7ee894ca4..75e9c9f77 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NZAxioms.
 Require Import NMake. (* contains W0Type *)
 Require Import ZnZ.
@@ -24,17 +36,17 @@ Definition NZplus := w_op.(znz_add).
 Definition NZminus := w_op.(znz_sub).
 Definition NZtimes := w_op.(znz_mul).
 
-Theorem NZE_equiv : equiv NZ NZeq.
+Theorem NZeq_equiv : equiv NZ NZeq.
 Proof.
 unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto.
 now transitivity [| y |].
 Qed.
 
 Add Relation NZ NZeq
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+as NZeq_rel.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 89f44fcd4..9c9161e2b 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NumPrelude.
 
 Module Type NZAxiomsSig.
@@ -11,12 +23,12 @@ Parameter Inline NZplus : NZ -> NZ -> NZ.
 Parameter Inline NZminus : NZ -> NZ -> NZ.
 Parameter Inline NZtimes : NZ -> NZ -> NZ.
 
-Axiom NZE_equiv : equiv NZ NZeq.
+Axiom NZeq_equiv : equiv NZ NZeq.
 Add Relation NZ NZeq
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+as NZeq_rel.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
@@ -59,9 +71,13 @@ Open Local Scope NatIntScope.
 
 Parameter Inline NZlt : NZ -> NZ -> Prop.
 Parameter Inline NZle : NZ -> NZ -> Prop.
+Parameter Inline NZmin : NZ -> NZ -> NZ.
+Parameter Inline NZmax : NZ -> NZ -> NZ.
 
 Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
 Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
+Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
+Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
 
 Notation "x < y" := (NZlt x y) : NatIntScope.
 Notation "x <= y" := (NZle x y) : NatIntScope.
@@ -71,4 +87,10 @@ Notation "x >= y" := (NZle y x) (only parsing) : NatIntScope.
 Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
 Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
 Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m.
+
+Axiom NZmin_l : forall n m : NZ, n <= m -> NZmin n m == n.
+Axiom NZmin_r : forall n m : NZ, m <= n -> NZmin n m == m.
+Axiom NZmax_l : forall n m : NZ, m <= n -> NZmax n m == n.
+Axiom NZmax_r : forall n m : NZ, n <= m -> NZmax n m == m.
+
 End NZOrdAxiomsSig.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index c467816d7..d8a9f0687 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import NZAxioms.
 
 Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig).
@@ -15,7 +27,7 @@ Qed.
 
 Declare Left Step NZE_stepl.
 (* The right step lemma is just the transitivity of NZeq *)
-Declare Right Step (proj1 (proj2 NZE_equiv)).
+Declare Right Step (proj1 (proj2 NZeq_equiv)).
 
 Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.
 Proof.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index c0ad96de3..854542906 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import NZAxioms.
 Require Import NZTimes.
 
@@ -216,7 +228,7 @@ assumption. false_hyp H1 H.
 intro H1; now apply H1.
 Qed.
 
-Theorem NZneq_lt_gt_cases : forall n m : NZ, n ~= m <-> n < m \/ n > m.
+Theorem NZlt_gt_cases : forall n m : NZ, n ~= m <-> n < m \/ n > m.
 Proof.
 intros n m; split.
 pose proof (NZlt_trichotomy n m); tauto.
@@ -231,11 +243,18 @@ Qed.
 
 (* The following theorem is cleary redundant, but helps not to
 remember whether one has to say le_gt_cases or lt_ge_cases *)
+
 Theorem NZlt_ge_cases : forall n m : NZ, n < m \/ n >= m.
 Proof.
 intros n m; destruct (NZle_gt_cases m n); try (now left); try (now right).
 Qed.
 
+Theorem NZle_ge_cases : forall n m : NZ, n <= m \/ n >= m.
+Proof.
+intros n m; destruct (NZle_gt_cases n m) as [H | H].
+now left. right; le_less.
+Qed.
+
 Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m.
 Proof.
 intros n m. split; intro H; [intro H1 |].
diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v
index 4380cb1b6..7a4c7719b 100644
--- a/theories/Numbers/NatInt/NZPlus.v
+++ b/theories/Numbers/NatInt/NZPlus.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import NZAxioms.
 Require Import NZBase.
 
diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v
index 517a8b7ff..e0d1f6350 100644
--- a/theories/Numbers/NatInt/NZTimes.v
+++ b/theories/Numbers/NatInt/NZTimes.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import NZAxioms.
 Require Import NZPlus.
 
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 2f3cf678b..6fc0078c0 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import NZAxioms.
 Require Import NZOrder.
 
@@ -239,13 +251,13 @@ Theorem NZtimes_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n ==
 Proof.
 intros n m p H; split; intro H1.
 destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]].
-apply -> NZeq_dne; intro H3. apply -> NZneq_lt_gt_cases in H3. destruct H3 as [H3 | H3].
+apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
 assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_neg_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 false_hyp H2 H.
-apply -> NZeq_dne; intro H3. apply -> NZneq_lt_gt_cases in H3. destruct H3 as [H3 | H3].
+apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
 assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |].
@@ -253,6 +265,11 @@ rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 now rewrite H1.
 Qed.
 
+Theorem NZtimes_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m).
+Proof.
+intros n m p. rewrite (NZtimes_comm n p), (NZtimes_comm m p); apply NZtimes_cancel_l.
+Qed.
+
 Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
 intros n m p H; do 2 rewrite NZle_lt_or_eq.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 052a18c3e..7cfff8e03 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NZAxioms.
 
 Set Implicit Arguments.
@@ -17,8 +29,10 @@ Notation times := NZtimes.
 Notation minus := NZminus.
 Notation lt := NZlt.
 Notation le := NZle.
-Notation "x == y"  := (NZeq x y) (at level 70) : NatScope.
-Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatScope.
+Notation min := NZmin.
+Notation max := NZmax.
+Notation "x == y"  := (Neq x y) (at level 70) : NatScope.
+Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope.
 Notation "0" := NZ0 : NatScope.
 Notation "1" := (NZsucc NZ0) : NatScope.
 Notation "x + y" := (NZplus x y) : NatScope.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 7c4464632..35d929f0c 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -1,7 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NAxioms.
 Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *)
 
-Module NBasePropFunct (Export NAxiomsMod : NAxiomsSig).
+Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig).
 
 Open Local Scope NatScope.
 
@@ -44,12 +56,15 @@ Proof NZsucc_inj_wd.
 Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
-(* Decidability of equality was proved only in NZOrder, but since it
-does not mention order, we'll put it here *)
+(* Decidability and stability of equality was proved only in NZOrder, but
+since it does not mention order, we'll put it here *)
 
 Theorem eq_em : forall n m : N, n == m \/ n ~= m.
 Proof NZeq_em.
 
+Theorem eq_dne : forall n m : N, ~ ~ n == m <-> n == m.
+Proof NZeq_dne.
+
 (* Now we prove that the successor of a number is not zero by defining a
 function (by recursion) that maps 0 to false and the successor to true *)
 
@@ -75,7 +90,7 @@ Qed.
 
 Implicit Arguments if_zero [A].
 
-Theorem neq_succ_0 : forall n : N, ~ S n == 0.
+Theorem neq_succ_0 : forall n : N, S n ~= 0.
 Proof.
 intros n H.
 assert (true = false); [| discriminate].
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 35e93bbc7..10c341cbf 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import NBase.
 
 Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index fe0ec4e62..f7abb82d8 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NTimesOrder.
 
 Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig).
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 8f68716bb..bc3aace38 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NTimes.
 
 Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
@@ -16,6 +28,14 @@ Theorem le_wd :
   forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
 Proof NZle_wd.
 
+Theorem min_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> min n1 m1 == min n2 m2.
+Proof NZmin_wd.
+
+Theorem max_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> max n1 m1 == max n2 m2.
+Proof NZmax_wd.
+
 Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n == m.
 Proof NZle_lt_or_eq.
 
@@ -25,6 +45,18 @@ Proof NZlt_irrefl.
 Theorem lt_succ_le : forall n m : N, n < S m <-> n <= m.
 Proof NZlt_succ_le.
 
+Theorem min_l : forall n m : N, n <= m -> min n m == n.
+Proof NZmin_l.
+
+Theorem min_r : forall n m : N, m <= n -> min n m == m.
+Proof NZmin_r.
+
+Theorem max_l : forall n m : N, m <= n -> max n m == n.
+Proof NZmax_l.
+
+Theorem max_r : forall n m : N, n <= m -> max n m == m.
+Proof NZmax_r.
+
 (* Renaming theorems from NZOrder.v *)
 
 Theorem lt_le_incl : forall n m : N, n < m -> n <= m.
@@ -101,12 +133,18 @@ Proof NZle_antisymm.
 Theorem lt_trichotomy : forall n m : N,  n < m \/ n == m \/ m < n.
 Proof NZlt_trichotomy.
 
+Theorem lt_gt_cases : forall n m : N, n ~= m <-> n < m \/ n > m.
+Proof NZlt_gt_cases.
+
 Theorem le_gt_cases : forall n m : N, n <= m \/ n > m.
 Proof NZle_gt_cases.
 
 Theorem lt_ge_cases : forall n m : N, n < m \/ n >= m.
 Proof NZlt_ge_cases.
 
+Theorem le_ge_cases : forall n m : N, n <= m \/ n >= m.
+Proof NZle_ge_cases.
+
 Theorem le_ngt : forall n m : N, n <= m <-> ~ n > m.
 Proof NZle_ngt.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 1e5c2211f..32912a73d 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -1,7 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NBase.
 
 Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
+
 Open Local Scope NatScope.
 
 Theorem plus_wd :
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index 76b85ee87..6a22e476d 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -1,6 +1,15 @@
-Require Export Ring.
-(* Since we define a ring below, it should be possible to call the tactic
-ring in the modules that use this module. Hence Export, not Import. *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NPlus.
 
 Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig).
@@ -43,21 +52,6 @@ Proof NZtimes_1_l.
 Theorem times_1_r : forall n : N, n * 1 == n.
 Proof NZtimes_1_r.
 
-Lemma Nsemi_ring : semi_ring_theory 0 1 NZplus NZtimes Neq.
-Proof.
-constructor.
-exact plus_0_l.
-exact plus_comm.
-exact plus_assoc.
-exact times_1_l.
-exact times_0_l.
-exact times_comm.
-exact times_assoc.
-exact times_plus_distr_r.
-Qed.
-
-Add Ring NSR : Nsemi_ring.
-
 (** Theorems that cannot be proved in NZTimes *)
 
 Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0.
@@ -70,7 +64,7 @@ intros m IH H1. rewrite times_succ_l in H1.
 rewrite plus_succ_r in H1. now apply neq_succ_0 in H1.
 Qed.
 
-Theorem times_eq_1 : forall n m, n * m == 1 -> n == 1 /\ m == 1.
+Theorem times_eq_1 : forall n m : N, n * m == 1 -> n == 1 /\ m == 1.
 Proof.
 intros n m; induct n.
 intro H; rewrite times_0_l in H; symmetry in H; false_hyp H neq_succ_0.
@@ -86,32 +80,29 @@ Qed.
 integers constructed from pairs of natural numbers, we'll need the
 following fact about natural numbers:
 
-a * x + u == a * y + v -> x + y' == x' + y -> a * x' + u = a * y' + v  (2)
+a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u = a * m' + v
 
-Here x + y' == x' + y represents equality of integers (x, y) and
-(x', y'), since a pair of natural numbers represents their integer
-difference. On integers, the (2) could be proved by moving
-a * y to the left, factoring out a and replacing x - y by x' - y'.
-However, the whole point is that we are only in the process of
-constructing integers, so this has to be proved for natural numbers,
-where we cannot move terms from one side of an equation to the other.
-This can be proved using the cancellation law plus_cancel_l. *)
+Here n + m' == n' + m expresses equality of integers (n, m) and (n', m'),
+since a pair (a, b) of natural numbers represents the integer a - b. On
+integers, the formula above could be proved by moving a * m to the left,
+factoring out a and replacing n - m by n' - m'. However, the formula is
+required in the process of constructing integers, so it has to be proved
+for natural numbers, where terms cannot be moved from one side of an
+equation to the other. The proof uses the cancellation laws plus_cancel_l
+and plus_cancel_r. *)
 
-Theorem plus_times_repl_pair : forall a n m n' m' u v,
+Theorem plus_times_repl_pair : forall a n m n' m' u v : N,
   a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
 Proof.
 intros a n m n' m' u v H1 H2.
 apply (@NZtimes_wd a a) in H2; [| reflexivity].
 do 2 rewrite times_plus_distr_l in H2. symmetry in H2.
-assert (H3 : (a * n + u) + (a * n' + a * m) == (a * m + v) + (a * n + a * m'))
-  by now apply NZplus_wd.
-stepl (a * n + (u + a * n' + a * m)) in H3 by ring.
-stepr (a * n + (a * m + v + a * m')) in H3 by ring.
-apply -> plus_cancel_l in H3.
-stepl (a * m + (u + a * n')) in H3 by ring.
-stepr (a * m + (v + a * m')) in H3 by ring.
-apply -> plus_cancel_l in H3.
-stepl (u + a * n') by ring. now stepr (v + a * m') by ring.
+pose proof (NZplus_wd _ _ H1 _ _ H2) as H3.
+rewrite (plus_shuffle1 (a * m)), (plus_comm (a * m) (a * n)) in H3.
+do 2 rewrite <- plus_assoc in H3. apply -> plus_cancel_l in H3.
+rewrite (plus_assoc u), (plus_comm (a * m)) in H3.
+apply -> plus_cancel_r in H3.
+now rewrite (plus_comm (a * n') u), (plus_comm (a * m') v).
 Qed.
 
 End NTimesPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index e644304dc..ec010ecee 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NOrder.
 
 Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
@@ -85,18 +97,18 @@ Proof.
 intros; apply NZplus_nonneg_pos. apply le_0_l. assumption.
 Qed.
 
-(* The following property is similar to plus_repl_pair in NPlus.v
-and is used to prove the correctness of the definition of order
-on integers constructed from pairs of natural numbers *)
+(* The following property is used to prove the correctness of the
+definition of order on integers constructed from pairs of natural numbers *)
 
-Theorem plus_lt_repl_pair : forall n m n' m' u v,
+Theorem plus_lt_repl_pair : forall n m n' m' u v : N,
   n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
 Proof.
 intros n m n' m' u v H1 H2.
-symmetry in H2. assert (H3 : n' + m <= n + m'); [now le_equal |].
-assert (H4 : n + u + (n' + m) < m + v + (n + m')); [now apply plus_lt_le_mono |].
-stepl (n + (m + (n' + u))) in H4 by ring. stepr (n + (m + (m' + v))) in H4 by ring.
-now do 2 apply <- plus_lt_mono_l in H4.
+symmetry in H2. assert (H3 : n' + m <= n + m') by now le_equal.
+pose proof (plus_lt_le_mono _ _ _ _ H1 H3) as H4.
+rewrite (plus_shuffle2 n u), (plus_shuffle1 m v), (plus_comm m n) in H4.
+do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4.
+now rewrite (plus_comm n' u), (plus_comm m' v).
 Qed.
 
 (** Multiplication and order *)
@@ -124,6 +136,9 @@ Qed.
 Theorem times_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof NZtimes_cancel_l.
 
+Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
+Proof NZtimes_cancel_r.
+
 Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof NZtimes_le_mono_pos_l.
 
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
new file mode 100644
index 000000000..9a5ff0e4b
--- /dev/null
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -0,0 +1,409 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
+Require Import BinPos.
+Require Import NMinus.
+
+(** Definitions *)
+
+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 *)
+
+Module NBinaryAxiomsMod <: NAxiomsSig.
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ := N.
+Definition NZeq := (@eq N).
+Definition NZ0 := N0.
+Definition NZsucc := succ.
+Definition NZpred := pred.
+Definition NZplus := plus.
+Definition NZminus := minus.
+Definition NZtimes := times.
+
+Theorem NZeq_equiv : equiv N NZeq.
+Proof (eq_equiv N).
+
+Add Relation N NZeq
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+as NZeq_rel.
+
+Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem NZinduction :
+  forall A : NZ -> Prop, predicate_wd NZeq A ->
+    A N0 -> (forall n, A n <-> A (NZsucc n)) -> forall n : NZ, A n.
+Proof.
+intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS.
+Qed.
+
+Theorem NZpred_succ : forall n : NZ, NZpred (NZsucc 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.
+
+Theorem NZplus_0_l : forall n : NZ, N0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+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.
+simpl in |- *; reflexivity.
+simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
+Qed.
+
+Theorem NZminus_0_r : forall n : NZ, n - N0 = n.
+Proof.
+now destruct n.
+Qed.
+
+Theorem NZminus_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (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.
+
+Theorem NZtimes_0_r : forall n : NZ, n * N0 = N0.
+Proof.
+destruct n; reflexivity.
+Qed.
+
+Theorem NZtimes_succ_r : forall n m : NZ, n * (NZsucc m) = n * m + n.
+Proof.
+destruct n as [| n]; destruct m as [| m]; simpl; try reflexivity.
+now rewrite Pmult_1_r.
+now rewrite (Pmult_comm n (Psucc m)), Pmult_Sn_m, (Pplus_comm n), Pmult_comm.
+Qed.
+
+End NZAxiomsMod.
+
+Definition NZlt := lt.
+Definition NZle := le.
+Definition NZmin := min.
+Definition NZmax := max.
+
+Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
+Proof.
+unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
+Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
+Proof.
+unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
+Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem NZle_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m.
+Proof.
+intros n m. unfold le, lt. 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.
+Qed.
+
+Theorem NZlt_succ_le : 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;
+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].
+now rewrite H. now rewrite H, Pcompare_refl.
+apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1.
+right; now apply Pcompare_Eq_eq. now left. elimtype False; now apply H.
+Qed.
+
+Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n.
+Proof.
+unfold NZmin, min, le; 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.
+case_eq (n ?= m); intro H1; try reflexivity.
+now apply -> Ncompare_eq_correct.
+apply Ncompare_antisymm in H1. now elim H.
+Qed.
+
+Theorem NZmax_l : forall n m : N, m <= n -> NZmax n m = n.
+Proof.
+unfold NZmax, max, le; 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.
+Qed.
+
+Theorem NZmax_r : forall n m : N, n <= m -> NZmax n m = m.
+Proof.
+unfold NZmax, max, le; intros n m H.
+destruct (n ?= m); try reflexivity. now elim H.
+Qed.
+
+End NZOrdAxiomsMod.
+
+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.
+Proof.
+reflexivity.
+Qed.
+
+Theorem recursion_wd :
+forall (A : Set) (Aeq : relation A),
+  forall a a' : A, Aeq a a' ->
+    forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
+      forall x x' : N, x = x' ->
+        Aeq (recursion a f x) (recursion a' f' x').
+Proof.
+unfold fun2_wd, NZeq, fun2_eq.
+intros A Aeq a a' Eaa' f f' Eff'.
+intro x; pattern x; apply Nrect.
+intros x' H; now rewrite <- H.
+clear x.
+intros x IH x' H; rewrite <- H.
+unfold recursion in *. do 2 rewrite Nrect_step.
+now apply Eff'; [| apply IH].
+Qed.
+
+Theorem recursion_0 :
+  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f N0 = a.
+Proof.
+intros A a f; unfold recursion; now rewrite Nrect_base.
+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)).
+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.
+clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
+now rewrite Nrect_step.
+Qed.
+
+End NBinaryAxiomsMod.
+
+Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod.
+
+(* Some fun comparing the efficiency of the generic log defined
+by strong (course-of-value) recursion and the log defined by recursion
+on notation *)
+(* Time Eval compute in (log 100000). *) (* 98 sec *)
+
+(*
+Fixpoint binposlog (p : positive) : N :=
+match p with
+| xH => 0
+| xO p' => Nsucc (binposlog p')
+| xI p' => Nsucc (binposlog p')
+end.
+
+Definition binlog (n : N) : N :=
+match n with
+| 0 => 0
+| Npos p => binposlog p
+end.
+*)
+(* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
+
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index abd98ebef..bf4432c38 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -1,195 +1,3 @@
-Require Import NArith.
-Require Import NMinus.
-
-Module NBinaryAxiomsMod <: NAxiomsSig.
-Open Local Scope N_scope.
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
-
-Definition NZ := N.
-Definition NZeq := (@eq N).
-Definition NZ0 := 0.
-Definition NZsucc := Nsucc.
-Definition NZpred := Npred.
-Definition NZplus := Nplus.
-Definition NZminus := Nminus.
-Definition NZtimes := Nmult.
-
-Theorem NZE_equiv : equiv N NZeq.
-Proof (eq_equiv N).
-
-Add Relation N NZeq
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
-Proof.
-congruence.
-Qed.
-
-Theorem NZinduction :
-  forall A : N -> Prop, predicate_wd NZeq A ->
-    A 0 -> (forall n, A n <-> A (Nsucc n)) -> forall n : N, A n.
-Proof.
-intros A A_wd A0 AS. apply Nind. assumption. intros; now apply -> AS.
-Qed.
-
-Theorem NZpred_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.
-
-Theorem NZplus_0_l : forall n : N, 0 + n = n.
-Proof Nplus_0_l.
-
-Theorem NZplus_succ_l : forall n m : N, (Nsucc n) + m = Nsucc (n + m).
-Proof Nplus_succ.
-
-Theorem NZminus_0_r : forall n : N, n - 0 = n.
-Proof Nminus_0_r.
-
-Theorem NZminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m).
-Proof Nminus_succ_r.
-
-Theorem NZtimes_0_r : forall n : N, n * 0 = 0.
-Proof.
-intro n; rewrite Nmult_comm; apply Nmult_0_l.
-Qed.
-
-Theorem NZtimes_succ_r : forall n m : N, n * (Nsucc m) = n * m + n.
-Proof.
-intros n m; rewrite Nmult_comm, Nmult_Sn_m.
-now rewrite Nplus_comm, Nmult_comm.
-Qed.
-
-End NZAxiomsMod.
-
-Definition NZlt := Nlt.
-Definition NZle := Nle.
-
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Theorem NZle_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m.
-Proof.
-intros n m.
-assert (H : (n ?= m) = Eq <-> n = m).
-split; intro H; [now apply Ncompare_Eq_eq | rewrite H; apply Ncompare_refl].
-unfold Nle, Nlt. rewrite <- H.
-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 : N, ~ n < n.
-Proof Nlt_irrefl.
-
-Theorem NZlt_succ_le : forall n m : N, n < (Nsucc m) <-> n <= m.
-Proof.
-intros x y. rewrite NZle_lt_or_eq.
-unfold Nlt, Nle; apply Ncompare_n_Sm.
-Qed.
-
-End NZOrdAxiomsMod.
-
-Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
-  Nrec (fun _ => A) a f n.
-Implicit Arguments recursion [A].
-
-Theorem succ_neq_0 : forall n : N, Nsucc n <> 0.
-Proof Nsucc_0.
-
-Theorem pred_0 : Npred 0 = 0.
-Proof.
-reflexivity.
-Qed.
-
-Theorem recursion_wd :
-forall (A : Set) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
-      forall x x' : N, x = x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
-Proof.
-unfold fun2_wd, NZeq, fun2_eq.
-intros A Aeq a a' Eaa' f f' Eff'.
-intro x; pattern x; apply Nind.
-intros x' H; now rewrite <- H.
-clear x.
-intros x IH x' H; rewrite <- H.
-unfold recursion, Nrec in *; do 2 rewrite Nrect_step.
-now apply Eff'; [| apply IH].
-Qed.
-
-Theorem recursion_0 :
-  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
-Proof.
-intros A a f; unfold recursion; unfold Nrec; now rewrite Nrect_base.
-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 (Nsucc n)) (f n (recursion a f n)).
-Proof.
-unfold NZeq, recursion, Nrec, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nind.
-rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.
-clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
-now rewrite Nrect_step.
-Qed.
-
-End NBinaryAxiomsMod.
-
-Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod.
-
-(* Some fun comparing the efficiency of the generic log defined
-by strong (course-of-value) recursion and the log defined by recursion
-on notation *)
-(* Time Eval compute in (log 100000). *) (* 98 sec *)
-
-(*
-Fixpoint binposlog (p : positive) : N :=
-match p with
-| xH => 0
-| xO p' => Nsucc (binposlog p')
-| xI p' => Nsucc (binposlog p')
-end.
-
-Definition binlog (n : N) : N :=
-match n with
-| 0 => 0
-| Npos p => binposlog p
-end.
-*)
-(* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
+Require Export NBinDefs.
+Require Export NArithRing.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0a59ab520..14899ed1d 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -1,4 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import Arith.
+Require Import Min.
+Require Import Max.
 Require Import NMinus.
 
 Module NPeanoAxiomsMod <: NAxiomsSig.
@@ -14,14 +28,14 @@ Definition NZplus := plus.
 Definition NZminus := minus.
 Definition NZtimes := mult.
 
-Theorem NZE_equiv : equiv nat NZeq.
+Theorem NZeq_equiv : equiv nat NZeq.
 Proof (eq_equiv nat).
 
 Add Relation nat NZeq
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+as NZeq_rel.
 
 (* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZeq"
 then the theorem generated for succ_wd below is forall x, succ x = succ x,
@@ -98,6 +112,8 @@ End NZAxiomsMod.
 
 Definition NZlt := lt.
 Definition NZle := le.
+Definition NZmin := min.
+Definition NZmax := max.
 
 Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
 Proof.
@@ -109,6 +125,16 @@ Proof.
 unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
 Qed.
 
+Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
+Proof.
+congruence.
+Qed.
+
 Theorem NZle_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m.
 Proof.
 intros n m; split.
@@ -127,6 +153,26 @@ Proof.
 intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm].
 Qed.
 
+Theorem NZmin_l : forall n m : nat, n <= m -> NZmin n m = n.
+Proof.
+exact min_l.
+Qed.
+
+Theorem NZmin_r : forall n m : nat, m <= n -> NZmin n m = m.
+Proof.
+exact min_r.
+Qed.
+
+Theorem NZmax_l : forall n m : nat, m <= n -> NZmax n m = n.
+Proof.
+exact max_l.
+Qed.
+
+Theorem NZmax_r : forall n m : nat, n <= m -> NZmax n m = m.
+Proof.
+exact max_r.
+Qed.
+
 End NZOrdAxiomsMod.
 
 Definition recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A :=
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 5505efd49..663395389 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export Setoid.
 Require Export Bool.
 (* Standard library. Export, not Import, because if a file
diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v
index 439fc6847..4fc7ce197 100644
--- a/theories/Numbers/QRewrite.v
+++ b/theories/Numbers/QRewrite.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Import List.
 Require Import Setoid.
 
@@ -135,13 +147,13 @@ end.
 (* For testing *)
 
 (*Parameter E : nat -> nat -> Prop.
-Axiom E_equiv : equiv nat E.
+Axiom eq_equiv : equiv nat E.
 
 Add Relation nat E
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
+ reflexivity proved by (proj1 eq_equiv)
+ symmetry proved by (proj2 (proj2 eq_equiv))
+ transitivity proved by (proj1 (proj2 eq_equiv))
+as eq_rel.
 
 Notation "x == y" := (E x y) (at level 70).