Arith: full integration of the "Numbers" modular framework

 - The earlier proof-of-concept file NPeano (which instantiates
   the "Numbers" framework for nat) becomes now the entry point
   in the Arith lib, and gets renamed PeanoNat. It still provides
   an inner module "Nat" which sums up everything about type nat
   (functions, predicates and properties of them).
   This inner module Nat is usable as soon as you Require Import Arith,
   or just Arith_base, or simply PeanoNat.

 - Definitions of operations over type nat are now grouped in a new
   file Init/Nat.v. This file is meant to be used without "Import",
   hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
   starts (but no proofs about them).

 - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
   are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
   where here Nat is Init/Nat.v).

 - This Coq.Init.Nat module (with only pure definitions) is Include'd
   in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
   sometimes instead of just Nat (for instance when doing "Print plus").
   Normally it should be ok to just ignore these "Init" since
   Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
   it's possible to get rid of these "Init" prefixes.

 - Concerning predicates, orders le and lt are still defined in Init/Peano.v,
   with their notations "<=" and "<". Properties in PeanoNat.Nat directly
   refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
   also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
   we cannot yet include an Inductive to implement a Parameter), but these
   aliased predicates won't probably be very convenient to use.

 - Technical remark: I've split the previous property functor NProp in
   two parts (NBasicProp and NExtraProp), it helps a lot for building
   PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:

   Module Nat.
     Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
     ... (** proofs of specifications for basic ops such as + * - *)
     Include NBasicProp. (** generic properties of these basic ops *)
     ... (** proofs of specifications for advanced ops (pow sqrt log2...)
             that may rely on proofs for + * - *)
     Include NExtraProp. (** all remaining properties *)
   End Nat.

- All other files in directory Arith are now taking advantage of PeanoNat :
  they are now filled with compatibility notations (when earlier lemmas
  have exact counterpart in the Nat module) or lemmas with one-line proofs
  based on the Nat module. All hints for database "arith" remain declared
  in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
  files are still Require'd (or not) by Arith.v, just as before.

- Compatibility should be almost complete. For instance in the stdlib,
  the only adaptations were due to .ml code referring to some Coq constant
  name such as Coq.Init.Peano.pred, which doesn't live well with the
  new compatibility notations.

4 files changed, 170 insertions, 217 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 256dce782..a8b086e77 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -8,7 +8,7 @@
 
 Require Export BinNums.
 Require Import BinPos RelationClasses Morphisms Setoid
- Equalities OrdersFacts GenericMinMax Bool NAxioms NProperties.
+ Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties.
 Require BinNatDef.
 
 (**********************************************************************)
@@ -66,6 +66,20 @@ Notation "( p | q )" := (divide p q) (at level 0) : N_scope.
 Definition Even n := exists m, n = 2*m.
 Definition Odd n := exists m, n = 2*m+1.
 
+(** Proofs of morphisms, obvious since eq is Leibniz *)
+
+Local Obligation Tactic := simpl_relation.
+Program Definition succ_wd : Proper (eq==>eq) succ := _.
+Program Definition pred_wd : Proper (eq==>eq) pred := _.
+Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
+Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
+Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
+Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
+Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
+Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
+Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
+Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+
 (** Decidability of equality. *)
 
 Definition eq_dec : forall n m : N, { n = m } + { n <> m }.
@@ -138,6 +152,50 @@ Proof.
 apply peano_rect_succ.
 Qed.
 
+(** Generic induction / recursion *)
+
+Theorem bi_induction :
+  forall A : N -> Prop, Proper (Logic.eq==>iff) A ->
+    A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
+Proof.
+intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS.
+Qed.
+
+Definition recursion {A} : A -> (N -> A -> A) -> N -> A :=
+  peano_rect (fun _ => A).
+
+Instance recursion_wd {A} (Aeq : relation A) :
+ Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion.
+Proof.
+intros a a' Ea f f' Ef x x' Ex. subst x'.
+induction x using peano_ind.
+trivial.
+unfold recursion in *. rewrite 2 peano_rect_succ. now apply Ef.
+Qed.
+
+Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a.
+Proof. reflexivity. Qed.
+
+Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A):
+ Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f ->
+  forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
+Proof.
+unfold recursion; intros a_wd f_wd n. induction n using peano_ind.
+rewrite peano_rect_succ. now apply f_wd.
+rewrite !peano_rect_succ in *. now apply f_wd.
+Qed.
+
+(** Specification of constants *)
+
+Lemma one_succ : 1 = succ 0.
+Proof. reflexivity. Qed.
+
+Lemma two_succ : 2 = succ 1.
+Proof. reflexivity. Qed.
+
+Definition pred_0 : pred 0 = 0.
+Proof. reflexivity. Qed.
+
 (** Properties of mixed successor and predecessor. *)
 
 Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p).
@@ -262,69 +320,30 @@ Qed.
 
 Include BoolOrderFacts.
 
-(** We regroup here some results used for proving the correctness
-    of more advanced functions. These results will also be provided
-    by the generic functor of properties about natural numbers
-    instantiated at the end of the file. *)
-
-Module Import Private_BootStrap.
-
-Theorem add_0_r n : n + 0 = n.
-Proof.
-now destruct n.
-Qed.
-
-Theorem add_comm n m : n + m = m + n.
-Proof.
-destruct n, m; simpl; try reflexivity. simpl. f_equal. apply Pos.add_comm.
-Qed.
-
-Theorem add_assoc n m p : n + (m + p) = n + m + p.
-Proof.
-destruct n; try reflexivity.
-destruct m; try reflexivity.
-destruct p; try reflexivity.
-simpl. f_equal. apply Pos.add_assoc.
-Qed.
-
-Lemma sub_add n m : n <= m -> m - n + n = m.
-Proof.
- destruct n as [|p], m as [|q]; simpl; try easy'. intros H.
- case Pos.sub_mask_spec; intros; simpl; subst; trivial.
- now rewrite Pos.add_comm.
- apply Pos.le_nlt in H. elim H. apply Pos.lt_add_r.
-Qed.
+(** Specification of minimum and maximum *)
 
-Theorem mul_comm n m : n * m = m * n.
+Theorem min_l n m : n <= m -> min n m = n.
 Proof.
-destruct n, m; simpl; trivial. f_equal. apply Pos.mul_comm.
+unfold min, le. case compare; trivial. now destruct 1.
 Qed.
 
-Lemma le_0_l n : 0<=n.
+Theorem min_r n m : m <= n -> min n m = m.
 Proof.
-now destruct n.
+unfold min, le. rewrite compare_antisym.
+case compare_spec; trivial. now destruct 2.
 Qed.
 
-Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m).
+Theorem max_l n m : m <= n -> max n m = n.
 Proof.
- unfold le, lt, leb. rewrite (compare_antisym n m).
- case compare; now constructor.
+unfold max, le. rewrite compare_antisym.
+case compare_spec; auto. now destruct 2.
 Qed.
 
-Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m.
+Theorem max_r n m : n <= m -> max n m = m.
 Proof.
- intro H. destruct p. simpl; auto.
- destruct n; destruct m.
- elim (Pos.lt_irrefl _ H).
- red; auto.
- rewrite add_0_r in H. simpl in H.
- red in H. simpl in H.
- elim (Pos.lt_not_add_l _ _ H).
- now apply (Pos.add_lt_mono_l p).
+unfold max, le. case compare; trivial. now destruct 1.
 Qed.
 
-End Private_BootStrap.
-
 (** Specification of lt and le. *)
 
 Lemma lt_succ_r n m : n < succ m <-> n<=m.
@@ -334,6 +353,13 @@ split. now destruct p. now destruct 1.
 apply Pos.lt_succ_r.
 Qed.
 
+(** We can now derive all properties of basic functions and orders,
+    and use these properties for proving the specs of more advanced
+    functions. *)
+
+Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+
+
 (** Properties of [double] and [succ_double] *)
 
 Lemma double_spec n : double n = 2 * n.
@@ -395,30 +421,6 @@ Proof.
 Qed.
 
 
-(** Specification of minimum and maximum *)
-
-Theorem min_l n m : n <= m -> min n m = n.
-Proof.
-unfold min, le. case compare; trivial. now destruct 1.
-Qed.
-
-Theorem min_r n m : m <= n -> min n m = m.
-Proof.
-unfold min, le. rewrite compare_antisym.
-case compare_spec; trivial. now destruct 2.
-Qed.
-
-Theorem max_l n m : m <= n -> max n m = n.
-Proof.
-unfold max, le. rewrite compare_antisym.
-case compare_spec; auto. now destruct 2.
-Qed.
-
-Theorem max_r n m : n <= m -> max n m = m.
-Proof.
-unfold max, le. case compare; trivial. now destruct 1.
-Qed.
-
 (** 0 is the least natural number *)
 
 Theorem compare_0_r n : (n ?= 0) <> Lt.
@@ -560,13 +562,13 @@ Proof.
   (* a~1 *)
   destruct pos_div_eucl as (q,r); simpl in *.
   case leb_spec; intros H; simpl; trivial.
-  apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial.
+  apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial.
   destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].
   apply (succ_double_lt _ _ IHa).
   (* a~0 *)
   destruct pos_div_eucl as (q,r); simpl in *.
   case leb_spec; intros H; simpl; trivial.
-  apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial.
+  apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial.
   destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].
   now destruct r.
   (* 1 *)
@@ -754,7 +756,7 @@ Proof.
  destruct m. now destruct (shiftl a n).
  rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l.
  apply IHn.
- apply add_lt_cancel_l with 1. rewrite 2 (add_succ_l 0). simpl.
+ apply add_lt_mono_l with 1. rewrite 2 (add_succ_l 0). simpl.
  now rewrite succ_pos_pred.
 Qed.
 
@@ -833,69 +835,10 @@ Proof.
  apply pos_ldiff_spec.
 Qed.
 
-(** Specification of constants *)
-
-Lemma one_succ : 1 = succ 0.
-Proof. reflexivity. Qed.
-
-Lemma two_succ : 2 = succ 1.
-Proof. reflexivity. Qed.
-
-Definition pred_0 : pred 0 = 0.
-Proof. reflexivity. Qed.
-
-(** Proofs of morphisms, obvious since eq is Leibniz *)
-
-Local Obligation Tactic := simpl_relation.
-Program Definition succ_wd : Proper (eq==>eq) succ := _.
-Program Definition pred_wd : Proper (eq==>eq) pred := _.
-Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
-Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
-Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
-Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
-Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
-Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
-Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
-Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
-
-(** Generic induction / recursion *)
-
-Theorem bi_induction :
-  forall A : N -> Prop, Proper (Logic.eq==>iff) A ->
-    A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
-Proof.
-intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS.
-Qed.
-
-Definition recursion {A} : A -> (N -> A -> A) -> N -> A :=
-  peano_rect (fun _ => A).
-
-Instance recursion_wd {A} (Aeq : relation A) :
- Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion.
-Proof.
-intros a a' Ea f f' Ef x x' Ex. subst x'.
-induction x using peano_ind.
-trivial.
-unfold recursion in *. rewrite 2 peano_rect_succ. now apply Ef.
-Qed.
-
-Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a.
-Proof. reflexivity. Qed.
-
-Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A):
- Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f ->
-  forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
-Proof.
-unfold recursion; intros a_wd f_wd n. induction n using peano_ind.
-rewrite peano_rect_succ. now apply f_wd.
-rewrite !peano_rect_succ in *. now apply f_wd.
-Qed.
-
-(** Instantiation of generic properties of natural numbers *)
+(** Instantiation of generic properties of advanced functions
+    (pow, sqrt, log2, div, gcd, ...) *)
 
-Include NProp
- <+ UsualMinMaxLogicalProperties
- <+ UsualMinMaxDecProperties.
+Include NExtraProp.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 6aeeccaf5..befcf7929 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -325,8 +325,8 @@ Definition lxor n m :=
 
 (** Shifts *)
 
-Definition shiftl_nat (a:N) := nat_rect _ a (fun _ => double).
-Definition shiftr_nat (a:N) := nat_rect _ a (fun _ => div2).
+Definition shiftl_nat (a:N)(n:nat) := Nat.iter n double a.
+Definition shiftr_nat (a:N)(n:nat) := Nat.iter n div2 a.
 
 Definition shiftl a n :=
   match a with
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 662c50abf..b36ea3204 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -6,8 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat
- Pnat Nnat Compare_dec Lt Minus.
+Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat.
 
 Local Open Scope N_scope.
 
@@ -111,10 +110,12 @@ Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
   N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n).
 Proof.
  induction n; intros m H.
- now rewrite <- minus_n_O.
- destruct m. inversion H. apply le_S_n in H.
- simpl. rewrite <- IHn; trivial.
- destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial.
+ - now rewrite Nat.sub_0_r.
+ - destruct m.
+   + inversion H.
+   + apply le_S_n in H.
+     simpl. rewrite <- IHn; trivial.
+     destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
 Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
@@ -123,9 +124,10 @@ Proof.
  induction n; intros m H. inversion H.
  rewrite Nshiftl_nat_S.
  destruct m.
- destruct (N.shiftl_nat a n); trivial.
- specialize (IHn m (lt_S_n _ _ H)).
- destruct (N.shiftl_nat a n); trivial.
+ - destruct (N.shiftl_nat a n); trivial.
+ - apply Lt.lt_S_n in H.
+   specialize (IHn m H).
+   destruct (N.shiftl_nat a n); trivial.
 Qed.
 
 (** A left shift for positive numbers (used in BigN) *)
@@ -446,49 +448,52 @@ Lemma Nless_trans :
    Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
 Proof.
   induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0.
-    case_eq (Nless N0 a'') ; intros Heqn. trivial.
-     rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0.
-    induction a' as [|a' _|a' _] using N.binary_ind.
-      rewrite (Nless_z (N.double a)) in H. discriminate H.
-      rewrite (Nless_def_1 a a') in H.
-       induction a'' using N.binary_ind.
-         rewrite (Nless_z (N.double a')) in H0. discriminate H0.
-         rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a'').
-          exact (IHa _ _ H H0).
-         apply Nless_def_3.
-      induction a'' as [|a'' _|a'' _] using N.binary_ind.
-        rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
-        rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
-        apply Nless_def_3.
-    induction a' as [|a' _|a' _] using N.binary_ind.
-      rewrite (Nless_z (N.succ_double a)) in H. discriminate H.
-      rewrite (Nless_def_4 a a') in H. discriminate H.
+  - case_eq (Nless N0 a'') ; intros Heqn.
+    + trivial.
+    + rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0.
+  - induction a' as [|a' _|a' _] using N.binary_ind.
+    + rewrite (Nless_z (N.double a)) in H. discriminate H.
+    + rewrite (Nless_def_1 a a') in H.
       induction a'' using N.binary_ind.
-        rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
-        rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
-        rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H.
-          rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0).
+      * rewrite (Nless_z (N.double a')) in H0. discriminate H0.
+      * rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a'').
+        exact (IHa _ _ H H0).
+      * apply Nless_def_3.
+    + induction a'' as [|a'' _|a'' _] using N.binary_ind.
+      * rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
+      * rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
+      * apply Nless_def_3.
+  - induction a' as [|a' _|a' _] using N.binary_ind.
+    + rewrite (Nless_z (N.succ_double a)) in H. discriminate H.
+    + rewrite (Nless_def_4 a a') in H. discriminate H.
+    + induction a'' using N.binary_ind.
+      * rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
+      * rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
+      * rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H.
+        rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0).
 Qed.
 
 Lemma Nless_total :
  forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
 Proof.
   induction a using N.binary_rec; intro a'.
-    case_eq (Nless N0 a') ; intros Heqb. left. left. auto.
-     right. rewrite (N0_less_2 a' Heqb). reflexivity.
-    induction a' as [|a' _|a' _] using N.binary_rec.
-      case_eq (Nless N0 (N.double a)) ; intros Heqb. left. right. auto.
-       right. exact (N0_less_2 _  Heqb).
-      rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
-        left. assumption.
-        right. reflexivity.
-    left. left. apply Nless_def_3.
-    induction a' as [|a' _|a' _] using N.binary_rec.
-      left. right. destruct a; reflexivity.
-      left. right. apply Nless_def_3.
-      rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->].
-        left. assumption.
-        right. reflexivity.
+  - case_eq (Nless N0 a') ; intros Heqb.
+    + left. left. auto.
+    + right. rewrite (N0_less_2 a' Heqb). reflexivity.
+  - induction a' as [|a' _|a' _] using N.binary_rec.
+    + case_eq (Nless N0 (N.double a)) ; intros Heqb.
+      * left. right. auto.
+      * right. exact (N0_less_2 _  Heqb).
+    + rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
+      * left. assumption.
+      * right. reflexivity.
+    + left. left. apply Nless_def_3.
+  - induction a' as [|a' _|a' _] using N.binary_rec.
+    + left. right. destruct a; reflexivity.
+    + left. right. apply Nless_def_3.
+    + rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->].
+      * left. assumption.
+      * right. reflexivity.
 Qed.
 
 (** Number of digits in a number *)
@@ -622,7 +627,7 @@ induction bv; intros.
 inversion H.
 destruct p ; simpl.
   destruct (Bv2N n bv); destruct h; simpl in *; auto.
-  specialize IHbv with p (lt_S_n _ _ H).
+  specialize IHbv with p (Lt.lt_S_n _ _ H).
     simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto.
 Qed.
 
@@ -641,7 +646,7 @@ Proof.
 destruct n as [|n].
 inversion H.
 induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto.
-intros H ; destruct (lt_n_O _ (lt_S_n _ _ H)).
+intros H ; destruct (Lt.lt_n_O _ (Lt.lt_S_n _ _ H)).
 Qed.
 
 (** Binary bitwise operations are the same in the two worlds. *)
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index cddc5f4cf..94242394b 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -6,8 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Minus Compare_dec Sumbool Div2 Min Max.
-Require Import BinPos BinNat Pnat.
+Require Import BinPos BinNat PeanoNat Pnat.
 
 (** * Conversions from [N] to [nat] *)
 
@@ -68,52 +67,58 @@ Qed.
 Lemma inj_sub a a' :
   N.to_nat (a - a') = N.to_nat a - N.to_nat a'.
 Proof.
- destruct a as [|a], a' as [|a']; simpl; auto with arith.
+ destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial.
  destruct (Pos.compare_spec a a').
- subst. now rewrite Pos.sub_mask_diag, <- minus_n_n.
- rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H.
- simpl; symmetry; apply not_le_minus_0; auto with arith.
- destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq).
- simpl. apply plus_minus. now rewrite <- Hq, Pos2Nat.inj_add.
+ - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag.
+ - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H.
+   simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl.
+ - destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq).
+   simpl; symmetry; apply Nat.add_sub_eq_l. now rewrite <- Hq, Pos2Nat.inj_add.
 Qed.
 
-Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a).
+Lemma inj_pred a : N.to_nat (N.pred a) = Nat.pred (N.to_nat a).
 Proof.
- intros. rewrite pred_of_minus, N.pred_sub. apply inj_sub.
+ rewrite <- Nat.sub_1_r, N.pred_sub. apply inj_sub.
 Qed.
 
-Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a).
+Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a).
 Proof.
  destruct a as [|[p|p| ]]; trivial.
- simpl N.to_nat. now rewrite Pos2Nat.inj_xI, div2_double_plus_one.
- simpl N.to_nat. now rewrite Pos2Nat.inj_xO, div2_double.
+ - simpl N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double.
+ - simpl N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double.
 Qed.
 
 Lemma inj_compare a a' :
- (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a').
+ (a ?= a')%N = (N.to_nat a ?= N.to_nat a').
 Proof.
  destruct a, a'; simpl; trivial.
- now destruct (Pos2Nat.is_succ p) as (n,->).
- now destruct (Pos2Nat.is_succ p) as (n,->).
- apply Pos2Nat.inj_compare.
+ - now destruct (Pos2Nat.is_succ p) as (n,->).
+ - now destruct (Pos2Nat.is_succ p) as (n,->).
+ - apply Pos2Nat.inj_compare.
 Qed.
 
 Lemma inj_max a a' :
-  N.to_nat (N.max a a') = max (N.to_nat a) (N.to_nat a').
+  N.to_nat (N.max a a') = Nat.max (N.to_nat a) (N.to_nat a').
 Proof.
  unfold N.max. rewrite inj_compare; symmetry.
- case nat_compare_spec; intros H; try rewrite H; auto with arith.
+ case Nat.compare_spec; intros.
+ - now apply Nat.max_r, Nat.eq_le_incl.
+ - now apply Nat.max_r, Nat.lt_le_incl.
+ - now apply Nat.max_l, Nat.lt_le_incl.
 Qed.
 
 Lemma inj_min a a' :
-  N.to_nat (N.min a a') = min (N.to_nat a) (N.to_nat a').
+  N.to_nat (N.min a a') = Nat.min (N.to_nat a) (N.to_nat a').
 Proof.
   unfold N.min; rewrite inj_compare. symmetry.
-  case nat_compare_spec; intros H; try rewrite H; auto with arith.
+  case Nat.compare_spec; intros.
+ - now apply Nat.min_l, Nat.eq_le_incl.
+ - now apply Nat.min_l, Nat.lt_le_incl.
+ - now apply Nat.min_r, Nat.lt_le_incl.
 Qed.
 
 Lemma inj_iter a {A} (f:A->A) (x:A) :
-  N.iter a f x = nat_rect (fun _ => A) x (fun _ => f) (N.to_nat a).
+  N.iter a f x = Nat.iter (N.to_nat a) f x.
 Proof.
  destruct a as [|a]. trivial. apply Pos2Nat.inj_iter.
 Qed.
@@ -166,7 +171,7 @@ Proof. nat2N. Qed.
 Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n).
 Proof. nat2N. Qed.
 
-Lemma inj_pred n : N.of_nat (pred n) = N.pred (N.of_nat n).
+Lemma inj_pred n : N.of_nat (Nat.pred n) = N.pred (N.of_nat n).
 Proof. nat2N. Qed.
 
 Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N.
@@ -178,23 +183,23 @@ Proof. nat2N. Qed.
 Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N.
 Proof. nat2N. Qed.
 
-Lemma inj_div2 n : N.of_nat (div2 n) = N.div2 (N.of_nat n).
+Lemma inj_div2 n : N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n).
 Proof. nat2N. Qed.
 
 Lemma inj_compare n n' :
-  nat_compare n n' = (N.of_nat n ?= N.of_nat n')%N.
+  (n ?= n') = (N.of_nat n ?= N.of_nat n')%N.
 Proof. now rewrite N2Nat.inj_compare, !id. Qed.
 
 Lemma inj_min n n' :
-  N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n').
+  N.of_nat (Nat.min n n') = N.min (N.of_nat n) (N.of_nat n').
 Proof. nat2N. Qed.
 
 Lemma inj_max n n' :
-  N.of_nat (max n n') = N.max (N.of_nat n) (N.of_nat n').
+  N.of_nat (Nat.max n n') = N.max (N.of_nat n) (N.of_nat n').
 Proof. nat2N. Qed.
 
 Lemma inj_iter n {A} (f:A->A) (x:A) :
-  nat_rect (fun _ => A) x (fun _ => f) n = N.iter (N.of_nat n) f x.
+  Nat.iter n f x = N.iter (N.of_nat n) f x.
 Proof. now rewrite N2Nat.inj_iter, !id. Qed.
 
 End Nat2N.