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.

18 files changed, 1507 insertions, 1177 deletions

diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index 9f0f05db4..290ce548a 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Export PeanoNat.
+
 Require Export Le.
 Require Export Lt.
 Require Export Plus.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 76132aed0..bcf409e66 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,10 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Le.
-Require Import Lt.
-Require Import Gt.
-Require Import Decidable.
+Require Import Le Lt Gt Decidable PeanoNat.
 
 Local Open Scope nat_scope.
 
@@ -29,31 +26,31 @@ Defined.
 
 Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
 Proof.
-  intros; apply lt_eq_lt_dec; assumption.
+  now apply lt_eq_lt_dec.
 Defined.
 
 Definition le_lt_dec n m : {n <= m} + {m < n}.
 Proof.
   induction n in m |- *.
-  auto with arith.
-  destruct m.
-  auto with arith.
-  elim (IHn m); auto with arith.
+  - left; auto with arith.
+  - destruct m.
+    + right; auto with arith.
+    + elim (IHn m); [left|right]; auto with arith.
 Defined.
 
 Definition le_le_S_dec n m : {n <= m} + {S m <= n}.
 Proof.
-  intros; exact (le_lt_dec n m).
+  exact (le_lt_dec n m).
 Defined.
 
 Definition le_ge_dec n m : {n <= m} + {n >= m}.
 Proof.
-  intros; elim (le_lt_dec n m); auto with arith.
+  elim (le_lt_dec n m); auto with arith.
 Defined.
 
 Definition le_gt_dec n m : {n <= m} + {n > m}.
 Proof.
-  intros; exact (le_lt_dec n m).
+  exact (le_lt_dec n m).
 Defined.
 
 Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
@@ -62,162 +59,121 @@ Proof.
   intros; absurd (m < n); auto with arith.
 Defined.
 
-Theorem le_dec : forall n m, {n <= m} + {~ n <= m}.
+Theorem le_dec n m : {n <= m} + {~ n <= m}.
 Proof.
-  intros n m. destruct (le_gt_dec n m).
-   auto with arith.
-   right. apply gt_not_le. assumption.
+  destruct (le_gt_dec n m).
+  - now left.
+  - right. now apply gt_not_le.
 Defined.
 
-Theorem lt_dec : forall n m, {n < m} + {~ n < m}.
+Theorem lt_dec n m : {n < m} + {~ n < m}.
 Proof.
-  intros; apply le_dec.
+  apply le_dec.
 Defined.
 
-Theorem gt_dec : forall n m, {n > m} + {~ n > m}.
+Theorem gt_dec n m : {n > m} + {~ n > m}.
 Proof.
-  intros; apply lt_dec.
+  apply lt_dec.
 Defined.
 
-Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}.
+Theorem ge_dec n m : {n >= m} + {~ n >= m}.
 Proof.
-  intros; apply le_dec.
+  apply le_dec.
 Defined.
 
 (** Proofs of decidability *)
 
-Theorem dec_le : forall n m, decidable (n <= m).
+Theorem dec_le n m : decidable (n <= m).
 Proof.
-  intros n m; destruct (le_dec n m); unfold decidable; auto.
+  apply Nat.le_decidable.
 Qed.
 
-Theorem dec_lt : forall n m, decidable (n < m).
+Theorem dec_lt n m : decidable (n < m).
 Proof.
-  intros; apply dec_le.
+  apply Nat.lt_decidable.
 Qed.
 
-Theorem dec_gt : forall n m, decidable (n > m).
+Theorem dec_gt n m : decidable (n > m).
 Proof.
-  intros; apply dec_lt.
+  apply Nat.lt_decidable.
 Qed.
 
-Theorem dec_ge : forall n m, decidable (n >= m).
+Theorem dec_ge n m : decidable (n >= m).
 Proof.
-  intros; apply dec_le.
+  apply Nat.le_decidable.
 Qed.
 
-Theorem not_eq : forall n m, n <> m -> n < m \/ m < n.
+Theorem not_eq n m : n <> m -> n < m \/ m < n.
 Proof.
-  intros x y H; elim (lt_eq_lt_dec x y);
-    [ intros H1; elim H1;
-      [ auto with arith | intros H2; absurd (x = y); assumption ]
-      | auto with arith ].
+  apply Nat.lt_gt_cases.
 Qed.
 
-
-Theorem not_le : forall n m, ~ n <= m -> n > m.
+Theorem not_le n m : ~ n <= m -> n > m.
 Proof.
-  intros x y H; elim (le_gt_dec x y);
-    [ intros H1; absurd (x <= y); assumption | trivial with arith ].
+  apply Nat.nle_gt.
 Qed.
 
-Theorem not_gt : forall n m, ~ n > m -> n <= m.
+Theorem not_gt n m : ~ n > m -> n <= m.
 Proof.
-  intros x y H; elim (le_gt_dec x y);
-    [ trivial with arith | intros H1; absurd (x > y); assumption ].
+  apply Nat.nlt_ge.
 Qed.
 
-Theorem not_ge : forall n m, ~ n >= m -> n < m.
+Theorem not_ge n m : ~ n >= m -> n < m.
 Proof.
-  intros x y H; exact (not_le y x H).
+  apply Nat.nle_gt.
 Qed.
 
-Theorem not_lt : forall n m, ~ n < m -> n >= m.
+Theorem not_lt n m : ~ n < m -> n >= m.
 Proof.
-  intros x y H; exact (not_gt y x H).
+  apply Nat.nlt_ge.
 Qed.
 
 
-(** A ternary comparison function in the spirit of [Z.compare]. *)
+(** A ternary comparison function in the spirit of [Z.compare].
+    See now [Nat.compare] and its properties.
+    In scope [nat_scope], the notation for [Nat.compare] is "?=" *)
 
-Fixpoint nat_compare n m :=
-  match n, m with
-   | O, O => Eq
-   | O, S _ => Lt
-   | S _, O => Gt
-   | S n', S m' => nat_compare n' m'
-  end.
+Notation nat_compare := Nat.compare (compat "8.4").
 
-Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m.
-Proof.
- reflexivity.
-Qed.
+Notation nat_compare_spec := Nat.compare_spec (compat "8.4").
+Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.4").
+Notation nat_compare_S := Nat.compare_succ (compat "8.4").
 
-Lemma nat_compare_eq_iff : forall n m, nat_compare n m = Eq <-> n = m.
+Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt.
 Proof.
-  induction n; destruct m; simpl; split; auto; try discriminate;
-   destruct (IHn m); auto.
+ symmetry. apply Nat.compare_lt_iff.
 Qed.
 
-Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m.
+Lemma nat_compare_gt n m : n>m <-> (n ?= m) = Gt.
 Proof.
-  intros; apply -> nat_compare_eq_iff; auto.
+ symmetry. apply Nat.compare_gt_iff.
 Qed.
 
-Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt.
+Lemma nat_compare_le n m : n<=m <-> (n ?= m) <> Gt.
 Proof.
-  induction n; destruct m; simpl; split; auto with arith;
-   try solve [inversion 1].
-  destruct (IHn m); auto with arith.
-  destruct (IHn m); auto with arith.
+ symmetry. apply Nat.compare_le_iff.
 Qed.
 
-Lemma nat_compare_gt : forall n m, n>m <-> nat_compare n m = Gt.
+Lemma nat_compare_ge n m : n>=m <-> (n ?= m) <> Lt.
 Proof.
-  induction n; destruct m; simpl; split; auto with arith;
-   try solve [inversion 1].
-  destruct (IHn m); auto with arith.
-  destruct (IHn m); auto with arith.
+ symmetry. apply Nat.compare_ge_iff.
 Qed.
 
-Lemma nat_compare_le : forall n m, n<=m <-> nat_compare n m <> Gt.
-Proof.
-  split.
-  intros LE; contradict LE.
-   apply lt_not_le. apply <- nat_compare_gt; auto.
-  intros NGT. apply not_lt. contradict NGT.
-   apply -> nat_compare_gt; auto.
-Qed.
-
-Lemma nat_compare_ge : forall n m, n>=m <-> nat_compare n m <> Lt.
-Proof.
-  split.
-  intros GE; contradict GE.
-   apply lt_not_le. apply <- nat_compare_lt; auto.
-  intros NLT. apply not_lt. contradict NLT.
-   apply -> nat_compare_lt; auto.
-Qed.
+(** Some projections of the above equivalences. *)
 
-Lemma nat_compare_spec :
-  forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
+Lemma nat_compare_eq n m : (n ?= m) = Eq -> n = m.
 Proof.
- intros. 
- destruct (nat_compare x y) eqn:?; constructor.
- apply nat_compare_eq; auto.
- apply <- nat_compare_lt; auto.
- apply <- nat_compare_gt; auto.
+  apply Nat.compare_eq_iff.
 Qed.
 
-(** Some projections of the above equivalences. *)
-
-Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m.
+Lemma nat_compare_Lt_lt n m : (n ?= m) = Lt -> n<m.
 Proof.
-  intros; apply <- nat_compare_lt; auto.
+  apply Nat.compare_lt_iff.
 Qed.
 
-Lemma nat_compare_Gt_gt : forall n m, nat_compare n m = Gt -> n>m.
+Lemma nat_compare_Gt_gt n m : (n ?= m) = Gt -> n>m.
 Proof.
-  intros; apply <- nat_compare_gt; auto.
+  apply Nat.compare_gt_iff.
 Qed.
 
 (** A previous definition of [nat_compare] in terms of [lt_eq_lt_dec].
@@ -230,70 +186,48 @@ Definition nat_compare_alt (n m:nat) :=
     | inright _ => Gt
   end.
 
-Lemma nat_compare_equiv: forall n m,
- nat_compare n m = nat_compare_alt n m.
+Lemma nat_compare_equiv n m : (n ?= m) = nat_compare_alt n m.
 Proof.
-  intros; unfold nat_compare_alt; destruct lt_eq_lt_dec as [[LT|EQ]|GT].
-  apply -> nat_compare_lt; auto.
-  apply <- nat_compare_eq_iff; auto.
-  apply -> nat_compare_gt; auto.
+  unfold nat_compare_alt; destruct lt_eq_lt_dec as [[|]|].
+  - now apply Nat.compare_lt_iff.
+  - now apply Nat.compare_eq_iff.
+  - now apply Nat.compare_gt_iff.
 Qed.
 
+(** A boolean version of [le] over [nat].
+    See now [Nat.leb] and its properties.
+    In scope [nat_scope], the notation for [Nat.leb] is "<=?" *)
 
-(** A boolean version of [le] over [nat]. *)
-
-Fixpoint leb (m:nat) : nat -> bool :=
-  match m with
-    | O => fun _:nat => true
-    | S m' =>
-      fun n:nat => match n with
-                     | O => false
-                     | S n' => leb m' n'
-                   end
-  end.
+Notation leb := Nat.leb (compat "8.4").
 
-Lemma leb_correct : forall m n, m <= n -> leb m n = true.
-Proof.
-  induction m as [| m IHm]. trivial.
-  destruct n. intro H. elim (le_Sn_O _ H).
-  intros. simpl. apply IHm. apply le_S_n. assumption.
-Qed.
+Notation leb_iff := Nat.leb_le (compat "8.4").
 
-Lemma leb_complete : forall m n, leb m n = true -> m <= n.
+Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n.
 Proof.
-  induction m. trivial with arith.
-  destruct n. intro H. discriminate H.
-  auto with arith.
+ rewrite Nat.leb_nle. apply Nat.nle_gt.
 Qed.
 
-Lemma leb_iff : forall m n, leb m n = true <-> m <= n.
+Lemma leb_correct m n : m <= n -> (m <=? n) = true.
 Proof.
-  split; auto using leb_correct, leb_complete.
+ apply Nat.leb_le.
 Qed.
 
-Lemma leb_correct_conv : forall m n, m < n -> leb n m = false.
+Lemma leb_complete m n : (m <=? n) = true -> m <= n.
 Proof.
-  intros.
-  generalize (leb_complete n m).
-  destruct (leb n m); auto.
-  intros; elim (lt_not_le m n); auto.
+ apply Nat.leb_le.
 Qed.
 
-Lemma leb_complete_conv : forall m n, leb n m = false -> m < n.
+Lemma leb_correct_conv m n : m < n -> (n <=? m) = false.
 Proof.
-  intros m n EQ. apply not_le.
-  intro LE. apply leb_correct in LE. rewrite LE in EQ; discriminate.
+ apply leb_iff_conv.
 Qed.
 
-Lemma leb_iff_conv : forall m n, leb n m = false <-> m < n.
+Lemma leb_complete_conv m n : (n <=? m) = false -> m < n.
 Proof.
-  split; auto using leb_complete_conv, leb_correct_conv.
+ apply leb_iff_conv.
 Qed.
 
-Lemma leb_compare : forall n m, leb n m = true <-> nat_compare n m <> Gt.
+Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt.
 Proof.
- split; intros.
- apply -> nat_compare_le. auto using leb_complete.
- apply leb_correct. apply <- nat_compare_le; auto.
+ rewrite Nat.compare_le_iff. apply Nat.leb_le.
 Qed.
-
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 56115c7f0..8cef48b69 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,10 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Lt.
-Require Import Plus.
-Require Import Compare_dec.
-Require Import Even.
+(** Nota : this file is OBSOLETE, and left only for compatibility.
+    Please consider using [Nat.div2] directly, and results about it
+    (see file PeanoNat). *)
+
+Require Import PeanoNat Even.
 
 Local Open Scope nat_scope.
 
@@ -17,12 +18,7 @@ Implicit Type n : nat.
 
 (** Here we define [n/2] and prove some of its properties *)
 
-Fixpoint div2 n : nat :=
-  match n with
-  | O => 0
-  | S O => 0
-  | S (S n') => S (div2 n')
-  end.
+Notation div2 := Nat.div2 (compat "8.4").
 
 (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
     useful to prove the corresponding induction principle *)
@@ -31,53 +27,48 @@ Lemma ind_0_1_SS :
   forall P:nat -> Prop,
     P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
 Proof.
-  intros P H0 H1 Hn.
-  cut (forall n, P n /\ P (S n)).
-  intros H'n n. elim (H'n n). auto with arith.
-
-  induction n. auto with arith.
-  intros. elim IHn; auto with arith.
+  intros P H0 H1 H2.
+  fix 1.
+  destruct n as [|[|n]].
+  - exact H0.
+  - exact H1.
+  - apply H2, ind_0_1_SS.
 Qed.
 
 (** [0 <n  =>  n/2 < n] *)
 
-Lemma lt_div2 : forall n, 0 < n -> div2 n < n.
-Proof.
-  intro n. pattern n. apply ind_0_1_SS.
-  (* n = 0 *)
-  inversion 1.
-  (* n=1 *)
-  simpl; trivial.
-  (* n=S S n' *)
-  intro n'; case (zerop n').
-    intro n'_eq_0. rewrite n'_eq_0. auto with arith.
-    auto with arith.
-Qed.
+Lemma lt_div2 n : 0 < n -> div2 n < n.
+Proof. apply Nat.lt_div2. Qed.
 
 Hint Resolve lt_div2: arith.
 
 (** Properties related to the parity *)
 
-Lemma even_div2 : forall n, even n -> div2 n = div2 (S n)
-with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
+Lemma even_div2 n : even n -> div2 n = div2 (S n).
 Proof.
-  destruct n; intro H.
-    (* 0 *) trivial.
-    (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial.
-  destruct n; intro.
-    (* 0 *) inversion H.
-    (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
+ rewrite Even.even_equiv. intros (p,->).
+ rewrite Nat.div2_succ_double. apply Nat.div2_double.
 Qed.
 
-Lemma div2_even n : div2 n = div2 (S n) -> even n
-with div2_odd n : S (div2 n) = div2 (S n) -> odd n.
+Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n).
 Proof.
-{ destruct n; intro H.
-  - constructor.
-  - constructor. apply div2_odd. rewrite H. trivial. }
-{ destruct n; intro H.
-  - discriminate.
-  - constructor. apply div2_even. injection H as <-. trivial. }
+ rewrite Even.odd_equiv. intros (p,->).
+ rewrite Nat.add_1_r, Nat.div2_succ_double.
+ simpl. f_equal. symmetry. apply Nat.div2_double.
+Qed.
+
+Lemma div2_even n : div2 n = div2 (S n) -> even n.
+Proof.
+ destruct (even_or_odd n) as [Ev|Od]; trivial.
+ apply odd_div2 in Od. rewrite <- Od. intro Od'.
+ elim (n_Sn _ Od').
+Qed.
+
+Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n.
+Proof.
+ destruct (even_or_odd n) as [Ev|Od]; trivial.
+ apply even_div2 in Ev. rewrite <- Ev. intro Ev'.
+ symmetry in Ev'. elim (n_Sn _ Ev').
 Qed.
 
 Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
@@ -93,58 +84,52 @@ Qed.
 
 (** Properties related to the double ([2n]) *)
 
-Definition double n := n + n.
+Notation double := Nat.double (compat "8.4").
 
-Hint Unfold double: arith.
+Hint Unfold double Nat.double: arith.
 
-Lemma double_S : forall n, double (S n) = S (S (double n)).
+Lemma double_S n : double (S n) = S (S (double n)).
 Proof.
-  intro. unfold double. simpl. auto with arith.
+  apply Nat.add_succ_r.
 Qed.
 
-Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m.
+Lemma double_plus n m : double (n + m) = double n + double m.
 Proof.
-  intros m n. unfold double.
-  do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
-  reflexivity.
+  apply Nat.add_shuffle1.
 Qed.
 
 Hint Resolve double_S: arith.
 
-Lemma even_odd_double :
-  forall n,
-    (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
+Lemma even_odd_double n :
+  (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
 Proof.
-  intro n. pattern n. apply ind_0_1_SS.
-  (* n = 0 *)
-  split; split; auto with arith.
-  intro H. inversion H.
-  (* n = 1 *)
-  split; split; auto with arith.
-  intro H. inversion H. inversion H1.
-  (* n = (S (S n')) *)
-  intros. destruct H as ((IH1,IH2),(IH3,IH4)).
-  split; split.
-  intro H. inversion H. inversion H1.
-  simpl. rewrite (double_S (div2 n0)). auto with arith.
-  simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
-  intro H. inversion H. inversion H1.
-  simpl. rewrite (double_S (div2 n0)). auto with arith.
-  simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+  revert n. fix 1. destruct n as [|[|n]].
+  - (* n = 0 *)
+    split; split; auto with arith. inversion 1.
+  - (* n = 1 *)
+    split; split; auto with arith. inversion_clear 1. inversion H0.
+  - (* n = (S (S n')) *)
+    destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')).
+    split; split; simpl; rewrite ?double_S.
+    + inversion_clear 1. inversion_clear H0. auto.
+    + injection 1. auto with arith.
+    + inversion_clear 1. inversion_clear H0. auto.
+    + injection 1. auto with arith.
 Qed.
+
 (** Specializations *)
 
-Lemma even_double : forall n, even n -> n = double (div2 n).
-Proof fun n => proj1 (proj1 (even_odd_double n)).
+Lemma even_double n : even n -> n = double (div2 n).
+Proof proj1 (proj1 (even_odd_double n)).
 
-Lemma double_even : forall n, n = double (div2 n) -> even n.
-Proof fun n => proj2 (proj1 (even_odd_double n)).
+Lemma double_even n : n = double (div2 n) -> even n.
+Proof proj2 (proj1 (even_odd_double n)).
 
-Lemma odd_double : forall n, odd n -> n = S (double (div2 n)).
-Proof fun n => proj1 (proj2 (even_odd_double n)).
+Lemma odd_double n : odd n -> n = S (double (div2 n)).
+Proof proj1 (proj2 (even_odd_double n)).
 
-Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n.
-Proof fun n => proj2 (proj2 (even_odd_double n)).
+Lemma double_odd n : n = S (double (div2 n)) -> odd n.
+Proof proj2 (proj2 (even_odd_double n)).
 
 Hint Resolve even_double double_even odd_double double_odd: arith.
 
@@ -166,22 +151,8 @@ Defined.
 
 (** Doubling before dividing by two brings back to the initial number. *)
 
-Lemma div2_double : forall n:nat, div2 (2*n) = n.
-Proof.
-  induction n.
-  simpl; auto.
-  simpl.
-  replace (n+S(n+0)) with (S (2*n)).
-  f_equal; auto.
-  simpl; auto with arith.
-Qed.
+Lemma div2_double n : div2 (2*n) = n.
+Proof. apply Nat.div2_double. Qed.
 
-Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n.
-Proof.
-  induction n.
-  simpl; auto.
-  simpl.
-  replace (n+S(n+0)) with (S (2*n)).
-  f_equal; auto.
-  simpl; auto with arith.
-Qed.
+Lemma div2_double_plus_one n : div2 (S (2*n)) = n.
+Proof. apply Nat.div2_succ_double. Qed.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index ce8eb4785..699ac281e 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,11 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Equality on natural numbers *)
-
+Require Import PeanoNat.
 Local Open Scope nat_scope.
 
-Implicit Types m n x y : nat.
+(** Equality on natural numbers *)
 
 (** * Propositional equality  *)
 
@@ -22,28 +21,33 @@ Fixpoint eq_nat n m : Prop :=
     | S n1, S m1 => eq_nat n1 m1
   end.
 
-Theorem eq_nat_refl : forall n, eq_nat n n.
+Theorem eq_nat_refl n : eq_nat n n.
+Proof.
   induction n; simpl; auto.
 Qed.
 Hint Resolve eq_nat_refl: arith v62.
 
 (** [eq] restricted to [nat] and [eq_nat] are equivalent *)
 
-Lemma eq_eq_nat : forall n m, n = m -> eq_nat n m.
-  induction 1; trivial with arith.
+Theorem eq_nat_is_eq n m : eq_nat n m <-> n = m.
+Proof.
+  split.
+  - revert m; induction n; destruct m; simpl; contradiction || auto.
+  - intros <-; apply eq_nat_refl.
 Qed.
-Hint Immediate eq_eq_nat: arith v62.
 
-Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m.
-  induction n; induction m; simpl; contradiction || auto with arith.
+Lemma eq_eq_nat n m : n = m -> eq_nat n m.
+Proof.
+ apply eq_nat_is_eq.
 Qed.
-Hint Immediate eq_nat_eq: arith v62.
 
-Theorem eq_nat_is_eq : forall n m, eq_nat n m <-> n = m.
+Lemma eq_nat_eq n m : eq_nat n m -> n = m.
 Proof.
-  split; auto with arith.
+ apply eq_nat_is_eq.
 Qed.
 
+Hint Immediate eq_eq_nat eq_nat_eq: arith v62.
+
 Theorem eq_nat_elim :
   forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
 Proof.
@@ -52,63 +56,47 @@ Qed.
 
 Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.
 Proof.
-  induction n.
-  destruct m as [| n].
-  auto with arith.
-  intros; right; red; trivial with arith.
-  destruct m as [| n0].
-  right; red; auto with arith.
-  intros.
-  simpl.
-  apply IHn.
+  induction n; destruct m; simpl.
+  - left; trivial.
+  - right; intro; trivial.
+  - right; intro; trivial.
+  - apply IHn.
 Defined.
 
 
-(** * Boolean equality on [nat] *)
+(** * Boolean equality on [nat].
 
-Fixpoint beq_nat n m : bool :=
-  match n, m with
-    | O, O => true
-    | O, S _ => false
-    | S _, O => false
-    | S n1, S m1 => beq_nat n1 m1
-  end.
+   We reuse the one already defined in module [Nat].
+   In scope [nat_scope], the notation "=?" can be used. *)
 
-Lemma beq_nat_refl : forall n, true = beq_nat n n.
-Proof.
-  intro x; induction x; simpl; auto.
-Qed.
+Notation beq_nat := Nat.eqb (compat "8.4").
 
-Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y.
-Proof.
-  double induction x y; simpl.
-    reflexivity.
-    intros n H1 H2. discriminate H2.
-    intros n H1 H2. discriminate H2.
-    intros n H1 z H2 H3. case (H2 _ H3). reflexivity.
-Defined.
+Notation beq_nat_true_iff := Nat.eqb_eq (compat "8.4").
+Notation beq_nat_false_iff := Nat.eqb_neq (compat "8.4").
 
-Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y.
+Lemma beq_nat_refl n : true = (n =? n).
 Proof.
- induction x; destruct y; simpl; auto; intros; discriminate.
+ symmetry. apply Nat.eqb_refl.
 Qed.
 
-Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
+Lemma beq_nat_true n m : (n =? m) = true -> n=m.
 Proof.
- induction x; destruct y; simpl; auto; intros; discriminate.
+ apply Nat.eqb_eq.
 Qed.
 
-Lemma beq_nat_true_iff : forall x y, beq_nat x y = true <-> x=y.
+Lemma beq_nat_false n m : (n =? m) = false -> n<>m.
 Proof.
- split. apply beq_nat_true.
- intros; subst; symmetry; apply beq_nat_refl.
+ apply Nat.eqb_neq.
 Qed.
 
-Lemma beq_nat_false_iff : forall x y, beq_nat x y = false <-> x<>y.
+(** TODO: is it really useful here to have a Defined ?
+    Otherwise we could use Nat.eqb_eq *)
+
+Definition beq_nat_eq : forall n m, true = (n =? m) -> n = m.
 Proof.
- intros x y.
- split. apply beq_nat_false.
- generalize (beq_nat_true_iff x y).
- destruct beq_nat; auto.
- intros IFF NEQ. elim NEQ. apply IFF; auto.
-Qed.
+  induction n; destruct m; simpl.
+  - reflexivity.
+  - discriminate.
+  - discriminate.
+  - intros H. case (IHn _ H). reflexivity.
+Defined.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 4f679fe2b..050b45ed9 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,16 +6,22 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Nota : this file is OBSOLETE, and left only for compatibility.
+    Please consider instead predicates [Nat.Even] and [Nat.Odd]
+    and Boolean functions [Nat.even] and [Nat.odd]. *)
+
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
 
+Require Import PeanoNat.
+
 Local Open Scope nat_scope.
 
 Implicit Types m n : nat.
 
 
-(** * Definition of [even] and [odd], and basic facts *)
+(** * Inductive definition of [even] and [odd] *)
 
 Inductive even : nat -> Prop :=
   | even_O : even 0
@@ -26,225 +32,150 @@ with odd : nat -> Prop :=
 Hint Constructors even: arith.
 Hint Constructors odd: arith.
 
-Lemma even_or_odd : forall n, even n \/ odd n.
+(** * Equivalence with predicates [Nat.Even] and [Nat.odd] *)
+
+Lemma even_equiv : forall n, even n <-> Nat.Even n.
+Proof.
+ fix 1.
+ destruct n as [|[|n]]; simpl.
+ - split; [now exists 0 | constructor].
+ - split.
+   + inversion_clear 1. inversion_clear H0.
+   + now rewrite <- Nat.even_spec.
+ - rewrite Nat.Even_succ_succ, <- even_equiv.
+   split.
+   + inversion_clear 1. now inversion_clear H0.
+   + now do 2 constructor.
+Qed.
+
+Lemma odd_equiv : forall n, odd n <-> Nat.Odd n.
+Proof.
+ fix 1.
+ destruct n as [|[|n]]; simpl.
+ - split.
+   + inversion_clear 1.
+   + now rewrite <- Nat.odd_spec.
+ - split; [ now exists 0 | do 2 constructor ].
+ - rewrite Nat.Odd_succ_succ, <- odd_equiv.
+   split.
+   + inversion_clear 1. now inversion_clear H0.
+   + now do 2 constructor.
+Qed.
+
+(** Basic facts *)
+
+Lemma even_or_odd n : even n \/ odd n.
 Proof.
   induction n.
-    auto with arith.
-    elim IHn; auto with arith.
+  - auto with arith.
+  - elim IHn; auto with arith.
 Qed.
 
-Lemma even_odd_dec : forall n, {even n} + {odd n}.
+Lemma even_odd_dec n : {even n} + {odd n}.
 Proof.
   induction n.
-    auto with arith.
-    elim IHn; auto with arith.
+  - auto with arith.
+  - elim IHn; auto with arith.
 Defined.
 
-Lemma not_even_and_odd : forall n, even n -> odd n -> False.
+Lemma not_even_and_odd n : even n -> odd n -> False.
 Proof.
   induction n.
-    intros even_0 odd_0. inversion odd_0.
-    intros even_Sn odd_Sn. inversion even_Sn. inversion odd_Sn. auto with arith.
+  - intros Ev Od. inversion Od.
+  - intros Ev Od. inversion Ev. inversion Od. auto with arith.
 Qed.
 
 
 (** * Facts about [even] & [odd] wrt. [plus] *)
 
-Lemma even_plus_split : forall n m,
-  (even (n + m) -> even n /\ even m \/ odd n /\ odd m)
-with odd_plus_split : forall n m,
+Ltac parity2bool :=
+ rewrite ?even_equiv, ?odd_equiv, <- ?Nat.even_spec, <- ?Nat.odd_spec.
+
+Ltac parity_binop_spec :=
+ rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul.
+
+Ltac parity_binop :=
+ parity2bool; parity_binop_spec; unfold Nat.odd;
+ do 2 destruct Nat.even; simpl; tauto.
+
+
+Lemma even_plus_split n m :
+  even (n + m) -> even n /\ even m \/ odd n /\ odd m.
+Proof. parity_binop. Qed.
+
+Lemma odd_plus_split n m :
   odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
-Proof.
-intros. clear even_plus_split. destruct n; simpl in *.
- auto with arith.
- inversion_clear H;
-   apply odd_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
-intros. clear odd_plus_split. destruct n; simpl in *.
- auto with arith.
- inversion_clear H;
-   apply even_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
-Qed.
+Proof. parity_binop. Qed.
 
-Lemma even_even_plus : forall n m, even n -> even m -> even (n + m)
-with odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
-Proof.
-intros n m [|] ?. trivial. apply even_S, odd_plus_l; trivial.
-intros n m [] ?. apply odd_S, even_even_plus; trivial.
-Qed.
+Lemma even_even_plus n m : even n -> even m -> even (n + m).
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m)
-with odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
-Proof.
-intros n m [|] ?. trivial. apply odd_S, odd_even_plus; trivial.
-intros n m [] ?. apply even_S, odd_plus_r; trivial.
-Qed.
+Lemma odd_plus_l n m : odd n -> even m -> odd (n + m).
+Proof. parity_binop. Qed.
+
+Lemma odd_plus_r n m : even n -> odd m -> odd (n + m).
+Proof. parity_binop. Qed.
 
-Lemma even_plus_aux : forall n m,
+Lemma odd_even_plus n m : odd n -> odd m -> even (n + m).
+Proof. parity_binop. Qed.
+
+Lemma even_plus_aux n m :
     (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
     (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
-Proof.
-split; split; auto using odd_plus_split, even_plus_split.
-intros [[]|[]]; auto using odd_plus_r, odd_plus_l.
-intros [[]|[]]; auto using even_even_plus, odd_even_plus.
-Qed.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
+Lemma even_plus_even_inv_r n m : even (n + m) -> even n -> even m.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
+Lemma even_plus_even_inv_l n m : even (n + m) -> even m -> even n.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
+Lemma even_plus_odd_inv_r n m : even (n + m) -> odd n -> odd m.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
-Hint Resolve even_even_plus odd_even_plus: arith.
+Lemma even_plus_odd_inv_l n m : even (n + m) -> odd m -> odd n.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
+Lemma odd_plus_even_inv_l n m : odd (n + m) -> odd m -> even n.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
+Lemma odd_plus_even_inv_r n m : odd (n + m) -> odd n -> even m.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
+Lemma odd_plus_odd_inv_l n m : odd (n + m) -> even m -> odd n.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
-Hint Resolve odd_plus_l odd_plus_r: arith.
+Lemma odd_plus_odd_inv_r n m : odd (n + m) -> even n -> odd m.
+Proof. parity_binop. Qed.
 
 
 (** * Facts about [even] and [odd] wrt. [mult] *)
 
-Lemma even_mult_aux :
-  forall n m,
-    (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
-Proof.
-  intros n; elim n; simpl; auto with arith.
-  intros m; split; split; auto with arith.
-  intros H'; inversion H'.
-  intros H'; elim H'; auto.
-  intros n0 H' m; split; split; auto with arith.
-  intros H'0.
-  elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2;
-    case H'1; auto.
-  intros H'5; elim H'5; intros H'6 H'7; auto with arith.
-  split; auto with arith.
-  case (H' m).
-  intros H'8 H'9; case H'9.
-  intros H'10; case H'10; auto with arith.
-  intros H'11 H'12; case (not_even_and_odd m); auto with arith.
-  intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto.
-  case (H' m).
-  intros H'8 H'9; case H'9; auto.
-  intros H'0; elim H'0; intros H'1 H'2; clear H'0.
-  elim (even_plus_aux m (n0 * m)); auto.
-  intros H'0 H'3.
-  elim H'0.
-  intros H'4 H'5; apply H'5; auto.
-  left; split; auto with arith.
-  case (H' m).
-  intros H'6 H'7; elim H'7.
-  intros H'8 H'9; apply H'9.
-  left.
-  inversion H'1; auto.
-  intros H'0.
-  elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4.
-  intros H'1 H'2.
-  elim H'1; auto.
-  intros H; case H; auto.
-  intros H'5; elim H'5; intros H'6 H'7; auto with arith.
-  left.
-  case (H' m).
-  intros H'8; elim H'8.
-  intros H'9; elim H'9; auto with arith.
-  intros H'0; elim H'0; intros H'1.
-  case (even_or_odd m); intros H'2.
-  apply even_even_plus; auto.
-  case (H' m).
-  intros H H0; case H0; auto.
-  apply odd_even_plus; auto.
-  inversion H'1; case (H' m); auto.
-  intros H1; case H1; auto.
-  apply even_even_plus; auto.
-  case (H' m).
-  intros H H0; case H0; auto.
-Qed.
+Lemma even_mult_aux n m :
+  (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
+Proof. parity_binop. Qed.
 
-Lemma even_mult_l : forall n m, even n -> even (n * m).
-Proof.
-  intros n m; case (even_mult_aux n m); auto.
-  intros H H0; case H0; auto.
-Qed.
+Lemma even_mult_l n m : even n -> even (n * m).
+Proof. parity_binop. Qed.
 
-Lemma even_mult_r : forall n m, even m -> even (n * m).
-Proof.
-  intros n m; case (even_mult_aux n m); auto.
-  intros H H0; case H0; auto.
-Qed.
-Hint Resolve even_mult_l even_mult_r: arith.
+Lemma even_mult_r n m : even m -> even (n * m).
+Proof. parity_binop. Qed.
 
-Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m.
-Proof.
-  intros n m H' H'0.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'2.
-  intros H'3; elim H'3; auto.
-  intros H; case (not_even_and_odd n); auto.
-Qed.
+Lemma even_mult_inv_r n m : even (n * m) -> odd n -> even m.
+Proof. parity_binop. Qed.
 
-Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.
-Proof.
-  intros n m H' H'0.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'2.
-  intros H'3; elim H'3; auto.
-  intros H; case (not_even_and_odd m); auto.
-Qed.
+Lemma even_mult_inv_l n m : even (n * m) -> odd m -> even n.
+Proof. parity_binop. Qed.
 
-Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m).
-Proof.
-  intros n m; case (even_mult_aux n m); intros H; case H; auto.
-Qed.
-Hint Resolve even_mult_l even_mult_r odd_mult: arith.
+Lemma odd_mult n m : odd n -> odd m -> odd (n * m).
+Proof. parity_binop. Qed.
 
-Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n.
-Proof.
-  intros n m H'.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'1.
-  intros H'3; elim H'3; auto.
-Qed.
+Lemma odd_mult_inv_l n m : odd (n * m) -> odd n.
+Proof. parity_binop. Qed.
 
-Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m.
-Proof.
-  intros n m H'.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'1.
-  intros H'3; elim H'3; auto.
-Qed.
+Lemma odd_mult_inv_r n m : odd (n * m) -> odd m.
+Proof. parity_binop. Qed.
+
+Hint Resolve
+ even_even_plus odd_even_plus odd_plus_l odd_plus_r
+ even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 37aa1b2c5..d560b4af9 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Plus.
-Require Import Mult.
-Require Import Lt.
+Require Import PeanoNat Plus Mult Lt.
 Local Open Scope nat_scope.
 
 (** Factorial *)
@@ -21,28 +19,19 @@ Fixpoint fact (n:nat) : nat :=
 
 Arguments fact n%nat.
 
-Lemma lt_O_fact : forall n:nat, 0 < fact n.
+Lemma lt_O_fact n : 0 < fact n.
 Proof.
-  simple induction n; unfold lt; simpl; auto with arith.
+  induction n; simpl; auto with arith.
 Qed.
 
-Lemma fact_neq_0 : forall n:nat, fact n <> 0.
+Lemma fact_neq_0 n : fact n <> 0.
 Proof.
-  intro.
-  apply not_eq_sym.
-  apply lt_O_neq.
-  apply lt_O_fact.
+ apply Nat.neq_0_lt_0, lt_O_fact.
 Qed.
 
-Lemma fact_le : forall n m:nat, n <= m -> fact n <= fact m.
+Lemma fact_le n m : n <= m -> fact n <= fact m.
 Proof.
   induction 1.
-  apply le_n.
-  assert (1 * fact n <= S m * fact m).
-  apply mult_le_compat.
-  apply lt_le_S; apply lt_O_Sn.
-  assumption.
-  simpl (1 * fact n) in H0.
-  rewrite <- plus_n_O in H0.
-  assumption.
+  - apply le_n.
+  - simpl. transitivity (fact m). trivial. apply Nat.le_add_r.
 Qed.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 31b155071..d142f3105 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -6,149 +6,140 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
+(** Theorems about [gt] in [nat].
+
+ This file is DEPRECATED now, see module [PeanoNat.Nat] instead,
+ which favor [lt] over [gt].
+
+ [gt] is defined in [Init/Peano.v] as:
 <<
 Definition gt (n m:nat) := m < n.
 >>
 *)
 
-Require Import Le.
-Require Import Lt.
-Require Import Plus.
+Require Import PeanoNat Le Lt Plus.
 Local Open Scope nat_scope.
 
-Implicit Types m n p : nat.
-
 (** * Order and successor *)
 
-Theorem gt_Sn_O : forall n, S n > 0.
-Proof.
-  auto with arith.
-Qed.
-Hint Resolve gt_Sn_O: arith v62.
+Theorem gt_Sn_O n : S n > 0.
+Proof Nat.lt_0_succ _.
 
-Theorem gt_Sn_n : forall n, S n > n.
-Proof.
-  auto with arith.
-Qed.
-Hint Resolve gt_Sn_n: arith v62.
+Theorem gt_Sn_n n : S n > n.
+Proof Nat.lt_succ_diag_r _.
 
-Theorem gt_n_S : forall n m, n > m -> S n > S m.
+Theorem gt_n_S n m : n > m -> S n > S m.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Resolve gt_n_S: arith v62.
 
-Lemma gt_S_n : forall n m, S m > S n -> m > n.
+Lemma gt_S_n n m : S m > S n -> m > n.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Immediate gt_S_n: arith v62.
 
-Theorem gt_S : forall n m, S n > m -> n > m \/ m = n.
+Theorem gt_S n m : S n > m -> n > m \/ m = n.
 Proof.
-  intros n m H; unfold gt; apply le_lt_or_eq; auto with arith.
+ intro. now apply Nat.lt_eq_cases, Nat.succ_le_mono.
 Qed.
 
-Lemma gt_pred : forall n m, m > S n -> pred m > n.
+Lemma gt_pred n m : m > S n -> pred m > n.
 Proof.
-  auto with arith.
+ apply Nat.lt_succ_lt_pred.
 Qed.
-Hint Immediate gt_pred: arith v62.
 
 (** * Irreflexivity *)
 
-Lemma gt_irrefl : forall n, ~ n > n.
-Proof lt_irrefl.
-Hint Resolve gt_irrefl: arith v62.
+Lemma gt_irrefl n : ~ n > n.
+Proof Nat.lt_irrefl _.
 
 (** * Asymmetry *)
 
-Lemma gt_asym : forall n m, n > m -> ~ m > n.
-Proof fun n m => lt_asym m n.
-
-Hint Resolve gt_asym: arith v62.
+Lemma gt_asym n m : n > m -> ~ m > n.
+Proof Nat.lt_asymm _ _.
 
 (** * Relating strict and large orders *)
 
-Lemma le_not_gt : forall n m, n <= m -> ~ n > m.
-Proof le_not_lt.
-Hint Resolve le_not_gt: arith v62.
-
-Lemma gt_not_le : forall n m, n > m -> ~ n <= m.
+Lemma le_not_gt n m : n <= m -> ~ n > m.
 Proof.
-auto with arith.
+ apply Nat.le_ngt.
 Qed.
 
-Hint Resolve gt_not_le: arith v62.
+Lemma gt_not_le n m : n > m -> ~ n <= m.
+Proof.
+ apply Nat.lt_nge.
+Qed.
 
-Theorem le_S_gt : forall n m, S n <= m -> m > n.
+Theorem le_S_gt n m : S n <= m -> m > n.
 Proof.
-  auto with arith.
+ apply Nat.le_succ_l.
 Qed.
-Hint Immediate le_S_gt: arith v62.
 
-Lemma gt_S_le : forall n m, S m > n -> n <= m.
+Lemma gt_S_le n m : S m > n -> n <= m.
 Proof.
-  intros n p; exact (lt_n_Sm_le n p).
+ apply Nat.succ_le_mono.
 Qed.
-Hint Immediate gt_S_le: arith v62.
 
-Lemma gt_le_S : forall n m, m > n -> S n <= m.
+Lemma gt_le_S n m : m > n -> S n <= m.
 Proof.
-  auto with arith.
+ apply Nat.le_succ_l.
 Qed.
-Hint Resolve gt_le_S: arith v62.
 
-Lemma le_gt_S : forall n m, n <= m -> S m > n.
+Lemma le_gt_S n m : n <= m -> S m > n.
 Proof.
-  auto with arith.
+ apply Nat.succ_le_mono.
 Qed.
-Hint Resolve le_gt_S: arith v62.
 
 (** * Transitivity *)
 
-Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p.
+Theorem le_gt_trans n m p : m <= n -> m > p -> n > p.
 Proof.
-  red; intros; apply lt_le_trans with m; auto with arith.
+ intros. now apply Nat.lt_le_trans with m.
 Qed.
 
-Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p.
+Theorem gt_le_trans n m p : n > m -> p <= m -> n > p.
 Proof.
-  red; intros; apply le_lt_trans with m; auto with arith.
+ intros. now apply Nat.le_lt_trans with m.
 Qed.
 
-Lemma gt_trans : forall n m p, n > m -> m > p -> n > p.
+Lemma gt_trans n m p : n > m -> m > p -> n > p.
 Proof.
-  red; intros n m p H1 H2.
-  apply lt_trans with m; auto with arith.
+ intros. now apply Nat.lt_trans with m.
 Qed.
 
-Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p.
+Theorem gt_trans_S n m p : S n > m -> m > p -> n > p.
 Proof.
-  red; intros; apply lt_le_trans with m; auto with arith.
+ intros. apply Nat.lt_le_trans with m; trivial. now apply Nat.succ_le_mono.
 Qed.
 
-Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
-
 (** * Comparison to 0 *)
 
-Theorem gt_0_eq : forall n, n > 0 \/ 0 = n.
+Theorem gt_0_eq n : n > 0 \/ 0 = n.
 Proof.
-  intro n; apply gt_S; auto with arith.
+ destruct n; [now right | left; apply Nat.lt_0_succ].
 Qed.
 
 (** * Simplification and compatibility *)
 
-Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m.
+Lemma plus_gt_reg_l n m p : p + n > p + m -> n > m.
 Proof.
-  red; intros n m p H; apply plus_lt_reg_l with p; auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
 
-Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
+Lemma plus_gt_compat_l n m p : n > m -> p + n > p + m.
 Proof.
-  auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
+
+(** * Hints *)
+
+Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith v62.
+Hint Immediate gt_S_n gt_pred : arith v62.
+Hint Resolve gt_irrefl gt_asym : arith v62.
+Hint Resolve le_not_gt gt_not_le : arith v62.
+Hint Immediate le_S_gt gt_S_le : arith v62.
+Hint Resolve gt_le_S le_gt_S : arith v62.
+Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
 Hint Resolve plus_gt_compat_l: arith v62.
 
 (* begin hide *)
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index c3386787d..53bb5cde2 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -6,7 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
+(** Order on natural numbers.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [le] is defined in [Init/Peano.v] as:
 <<
 Inductive le (n:nat) : nat -> Prop :=
   | le_n : n <= n
@@ -14,110 +18,58 @@ Inductive le (n:nat) : nat -> Prop :=
 
 where "n <= m" := (le n m) : nat_scope.
 >>
- *)
+*)
 
-Local Open Scope nat_scope.
+Require Import PeanoNat.
 
-Implicit Types m n p : nat.
+Local Open Scope nat_scope.
 
-(** * [le] is a pre-order *)
+(** * [le] is an order on [nat] *)
 
-(** Reflexivity *)
-Theorem le_refl : forall n, n <= n.
-Proof.
-  exact le_n.
-Qed.
+Notation le_refl := Nat.le_refl (compat "8.4").
+Notation le_trans := Nat.le_trans (compat "8.4").
+Notation le_antisym := Nat.le_antisymm (compat "8.4").
 
-(** Transitivity *)
-Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
-Proof.
-  induction 2; auto.
-Qed.
 Hint Resolve le_trans: arith v62.
+Hint Immediate le_antisym: arith v62.
 
-(** * Properties of [le] w.r.t. successor, predecessor and 0 *)
-
-(** Comparison to 0 *)
-
-Theorem le_0_n : forall n, 0 <= n.
-Proof.
-  induction n; auto.
-Qed.
-
-Theorem le_Sn_0 : forall n, ~ S n <= 0.
-Proof.
-  red; intros n H.
-  change (IsSucc 0); elim H; simpl; auto with arith.
-Qed.
+(** * Properties of [le] w.r.t 0 *)
 
-Hint Resolve le_0_n le_Sn_0: arith v62.
+Notation le_0_n := Nat.le_0_l (compat "8.4").  (* 0 <= n *)
+Notation le_Sn_0 := Nat.nle_succ_0 (compat "8.4").  (* ~ S n <= 0 *)
 
-Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n.
+Lemma le_n_0_eq n : n <= 0 -> 0 = n.
 Proof.
-  induction n. auto with arith.  idtac. auto with arith.
-  intro; contradiction le_Sn_0 with n.
+ intros. symmetry. now apply Nat.le_0_r.
 Qed.
-Hint Immediate le_n_0_eq: arith v62.
 
+(** * Properties of [le] w.r.t successor *)
 
-(** [le] and successor *)
+(** See also [Nat.succ_le_mono]. *)
 
 Theorem le_n_S : forall n m, n <= m -> S n <= S m.
-Proof.
-  induction 1; auto.
-Qed.
+Proof Peano.le_n_S.
 
-Theorem le_n_Sn : forall n, n <= S n.
-Proof.
-  auto.
-Qed.
+Theorem le_S_n : forall n m, S n <= S m -> n <= m.
+Proof Peano.le_S_n.
 
-Hint Resolve le_n_S le_n_Sn : arith v62.
+Notation le_n_Sn := Nat.le_succ_diag_r (compat "8.4"). (* n <= S n *)
+Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *)
 
 Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
-Proof.
-  intros n m H; apply le_trans with (S n); auto with arith.
-Qed.
-Hint Immediate le_Sn_le: arith v62.
+Proof Nat.lt_le_incl.
 
-Theorem le_S_n : forall n m, S n <= S m -> n <= m.
-Proof.
-  exact Peano.le_S_n.
-Qed.
-Hint Immediate le_S_n: arith v62.
+Hint Resolve le_0_n le_Sn_0: arith v62.
+Hint Resolve le_n_S le_n_Sn le_Sn_n : arith v62.
+Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith v62.
 
-Theorem le_Sn_n : forall n, ~ S n <= n.
-Proof.
-  induction n; auto with arith.
-Qed.
-Hint Resolve le_Sn_n: arith v62.
+(** * Properties of [le] w.r.t predecessor *)
 
-(** [le] and predecessor *)
+Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *)
+Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *)
 
-Theorem le_pred_n : forall n, pred n <= n.
-Proof.
-  induction n; auto with arith.
-Qed.
 Hint Resolve le_pred_n: arith v62.
 
-Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
-Proof.
-  exact Peano.le_pred.
-Qed.
-
-(** * [le] is a order on [nat] *)
-(** Antisymmetry *)
-
-Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m.
-Proof.
-  intros n m H; destruct H as [|m' H]; auto with arith.
-  intros H1.
-  absurd (S m' <= m'); auto with arith.
-  apply le_trans with n; auto with arith.
-Qed.
-Hint Immediate le_antisym: arith v62.
-
-
 (** * A different elimination principle for the order on natural numbers *)
 
 Lemma le_elim_rel :
@@ -126,10 +78,10 @@ Lemma le_elim_rel :
    (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) ->
    forall n m, n <= m -> P n m.
 Proof.
-  induction n; auto with arith.
-  intros m Le.
-  elim Le; auto with arith.
-Qed.
+  intros P H0 HS.
+  induction n; trivial.
+  intros m Le. elim Le; auto with arith.
+ Qed.
 
 (* begin hide *)
 Notation le_O_n := le_0_n (only parsing).
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 8559b782b..5a793ffdd 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -6,185 +6,149 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
+(** Strict order on natural numbers.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [lt] is defined in library [Init/Peano.v] as:
 <<
 Definition lt (n m:nat) := S n <= m.
 Infix "<" := lt : nat_scope.
 >>
 *)
 
-Require Import Le.
-Local Open Scope nat_scope.
+Require Import PeanoNat.
 
-Implicit Types m n p : nat.
+Local Open Scope nat_scope.
 
 (** * Irreflexivity *)
 
-Theorem lt_irrefl : forall n, ~ n < n.
-Proof le_Sn_n.
+Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *)
+
 Hint Resolve lt_irrefl: arith v62.
 
 (** * Relationship between [le] and [lt] *)
 
-Theorem lt_le_S : forall n m, n < m -> S n <= m.
+Theorem lt_le_S n m : n < m -> S n <= m.
 Proof.
-  auto with arith.
+ apply Nat.le_succ_l.
 Qed.
-Hint Immediate lt_le_S: arith v62.
 
-Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m.
+Theorem lt_n_Sm_le n m : n < S m -> n <= m.
 Proof.
-  auto with arith.
+ apply Nat.lt_succ_r.
 Qed.
-Hint Immediate lt_n_Sm_le: arith v62.
 
-Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m.
+Theorem le_lt_n_Sm n m : n <= m -> n < S m.
 Proof.
-  auto with arith.
+ apply Nat.lt_succ_r.
 Qed.
+
+Hint Immediate lt_le_S: arith v62.
+Hint Immediate lt_n_Sm_le: arith v62.
 Hint Immediate le_lt_n_Sm: arith v62.
 
-Theorem le_not_lt : forall n m, n <= m -> ~ m < n.
+Theorem le_not_lt n m : n <= m -> ~ m < n.
 Proof.
-  induction 1; auto with arith.
+ apply Nat.le_ngt.
 Qed.
 
-Theorem lt_not_le : forall n m, n < m -> ~ m <= n.
+Theorem lt_not_le n m : n < m -> ~ m <= n.
 Proof.
-  red; intros n m Lt Le; exact (le_not_lt m n Le Lt).
+ apply Nat.lt_nge.
 Qed.
+
 Hint Immediate le_not_lt lt_not_le: arith v62.
 
 (** * Asymmetry *)
 
-Theorem lt_asym : forall n m, n < m -> ~ m < n.
-Proof.
-  induction 1; auto with arith.
-Qed.
+Notation lt_asym := Nat.lt_asymm (compat "8.4"). (* n<m -> ~m<n *)
 
-(** * Order and successor *)
+(** * Order and 0 *)
 
-Theorem lt_n_Sn : forall n, n < S n.
-Proof.
-  auto with arith.
-Qed.
-Hint Resolve lt_n_Sn: arith v62.
+Notation lt_0_Sn := Nat.lt_0_succ (compat "8.4"). (* 0 < S n *)
+Notation lt_n_0 := Nat.nlt_0_r (compat "8.4"). (* ~ n < 0 *)
 
-Theorem lt_S : forall n m, n < m -> n < S m.
+Theorem neq_0_lt n : 0 <> n -> 0 < n.
 Proof.
-  auto with arith.
+ intros. now apply Nat.neq_0_lt_0, Nat.neq_sym.
 Qed.
-Hint Resolve lt_S: arith v62.
 
-Theorem lt_n_S : forall n m, n < m -> S n < S m.
+Theorem lt_0_neq n : 0 < n -> 0 <> n.
 Proof.
-  auto with arith.
+ intros. now apply Nat.neq_sym, Nat.neq_0_lt_0.
 Qed.
-Hint Resolve lt_n_S: arith v62.
 
-Theorem lt_S_n : forall n m, S n < S m -> n < m.
+Hint Resolve lt_0_Sn lt_n_0 : arith v62.
+Hint Immediate neq_0_lt lt_0_neq: arith v62.
+
+(** * Order and successor *)
+
+Notation lt_n_Sn := Nat.lt_succ_diag_r (compat "8.4"). (* n < S n *)
+Notation lt_S := Nat.lt_lt_succ_r (compat "8.4"). (* n < m -> n < S m *)
+
+Theorem lt_n_S n m : n < m -> S n < S m.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Immediate lt_S_n: arith v62.
 
-Theorem lt_0_Sn : forall n, 0 < S n.
+Theorem lt_S_n n m : S n < S m -> n < m.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Resolve lt_0_Sn: arith v62.
 
-Theorem lt_n_0 : forall n, ~ n < 0.
-Proof le_Sn_0.
-Hint Resolve lt_n_0: arith v62.
+Hint Resolve lt_n_Sn lt_S lt_n_S : arith v62.
+Hint Immediate lt_S_n : arith v62.
 
 (** * Predecessor *)
 
-Lemma S_pred : forall n m, m < n -> n = S (pred n).
+Lemma S_pred n m : m < n -> n = S (pred n).
 Proof.
-induction 1; auto with arith.
+ intros. symmetry. now apply Nat.lt_succ_pred with m.
 Qed.
 
-Lemma lt_pred : forall n m, S n < m -> n < pred m.
+Lemma lt_pred n m : S n < m -> n < pred m.
 Proof.
-induction 1; simpl; auto with arith.
+ apply Nat.lt_succ_lt_pred.
 Qed.
-Hint Immediate lt_pred: arith v62.
 
-Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n.
-destruct 1; simpl; auto with arith.
+Lemma lt_pred_n_n n : 0 < n -> pred n < n.
+Proof.
+ intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0.
 Qed.
+
+Hint Immediate lt_pred: arith v62.
 Hint Resolve lt_pred_n_n: arith v62.
 
 (** * Transitivity properties *)
 
-Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
-Proof.
-  induction 2; auto with arith.
-Qed.
-
-Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
-Proof.
-  induction 2; auto with arith.
-Qed.
-
-Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
-Proof.
-  induction 2; auto with arith.
-Qed.
+Notation lt_trans := Nat.lt_trans (compat "8.4").
+Notation lt_le_trans := Nat.lt_le_trans (compat "8.4").
+Notation le_lt_trans := Nat.le_lt_trans (compat "8.4").
 
 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62.
 
 (** * Large = strict or equal *)
 
-Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m.
-Proof.
-  induction 1; auto with arith.
-Qed.
+Notation le_lt_or_eq_iff := Nat.lt_eq_cases (compat "8.4").
 
-Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m.
 Proof.
-  split.
-  intros; apply le_lt_or_eq; auto.
-  destruct 1; subst; auto with arith.
+ apply Nat.lt_eq_cases.
 Qed.
 
-Theorem lt_le_weak : forall n m, n < m -> n <= m.
-Proof.
-  auto with arith.
-Qed.
+Notation lt_le_weak := Nat.lt_le_incl (compat "8.4").
+
 Hint Immediate lt_le_weak: arith v62.
 
 (** * Dichotomy *)
 
-Theorem le_or_lt : forall n m, n <= m \/ m < n.
-Proof.
-  intros n m; pattern n, m; apply nat_double_ind; auto with arith.
-  induction 1; auto with arith.
-Qed.
-
-Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n.
-Proof.
-  intros m n diff.
-  elim (le_or_lt n m); [ intro H'0 | auto with arith ].
-  elim (le_lt_or_eq n m); auto with arith.
-  intro H'; elim diff; auto with arith.
-Qed.
-
-(** * Comparison to 0 *)
+Notation le_or_lt := Nat.le_gt_cases (compat "8.4"). (* n <= m \/ m < n *)
 
-Theorem neq_0_lt : forall n, 0 <> n -> 0 < n.
+Theorem nat_total_order n m : n <> m -> n < m \/ m < n.
 Proof.
-  induction n; auto with arith.
-  intros; absurd (0 = 0); trivial with arith.
+ apply Nat.lt_gt_cases.
 Qed.
-Hint Immediate neq_0_lt: arith v62.
-
-Theorem lt_0_neq : forall n, 0 < n -> 0 <> n.
-Proof.
-  induction 1; auto with arith.
-Qed.
-Hint Immediate lt_0_neq: arith v62.
 
 (* begin hide *)
 Notation lt_O_Sn := lt_0_Sn (only parsing).
@@ -192,3 +156,7 @@ Notation neq_O_lt := neq_0_lt (only parsing).
 Notation lt_O_neq := lt_0_neq (only parsing).
 Notation lt_n_O := lt_n_0 (only parsing).
 (* end hide *)
+
+(** For compatibility, we "Require" the same files as before *)
+
+Require Import Le.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 5623564a2..d38ed7e4e 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *)
+(** THIS FILE IS DEPRECATED. Use [PeanoNat.Nat] instead. *)
 
-Require Import NPeano.
+Require Import PeanoNat.
 
 Local Open Scope nat_scope.
 Implicit Types m n p : nat.
 
-Notation max := Peano.max (only parsing).
+Notation max := Nat.max (only parsing).
 
 Definition max_0_l := Nat.max_0_l.
 Definition max_0_r := Nat.max_0_r.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index a2a7930df..115901792 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *)
+(** THIS FILE IS DEPRECATED. Use [PeanoNat.Nat] instead. *)
 
-Require Import NPeano.
+Require Import PeanoNat.
 
 Local Open Scope nat_scope.
 Implicit Types m n p : nat.
 
-Notation min := Peano.min (only parsing).
+Notation min := Nat.min (only parsing).
 
 Definition min_0_l := Nat.min_0_l.
 Definition min_0_r := Nat.min_0_r.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 480243311..cb6cc646f 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,151 +6,114 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
+(** Properties of subtraction between natural numbers.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [minus] is now an alias for [Nat.sub], which is defined in [Init/Nat.v] as:
 <<
-Fixpoint minus (n m:nat) : nat :=
+Fixpoint sub (n m:nat) : nat :=
   match n, m with
-  | O, _ => n
-  | S k, O => S k
   | S k, S l => k - l
+  | _, _ => n
   end
-where "n - m" := (minus n m) : nat_scope.
+where "n - m" := (sub n m) : nat_scope.
 >>
 *)
 
-Require Import Lt.
-Require Import Le.
+Require Import PeanoNat Lt Le.
 
 Local Open Scope nat_scope.
 
-Implicit Types m n p : nat.
-
 (** * 0 is right neutral *)
 
-Lemma minus_n_O : forall n, n = n - 0.
+Lemma minus_n_O n : n = n - 0.
 Proof.
-  induction n; simpl; auto with arith.
+ symmetry. apply Nat.sub_0_r.
 Qed.
-Hint Resolve minus_n_O: arith v62.
 
 (** * Permutation with successor *)
 
-Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
+Lemma minus_Sn_m n m : m <= n -> S (n - m) = S n - m.
 Proof.
-  intros n m Le; pattern m, n; apply le_elim_rel; simpl;
-    auto with arith.
+ intros. symmetry. now apply Nat.sub_succ_l.
 Qed.
-Hint Resolve minus_Sn_m: arith v62.
 
-Theorem pred_of_minus : forall n, pred n = n - 1.
+Theorem pred_of_minus n : pred n = n - 1.
 Proof.
-  intro x; induction x; simpl; auto with arith.
+ symmetry. apply Nat.sub_1_r.
 Qed.
 
 (** * Diagonal *)
 
-Lemma minus_diag : forall n, n - n = 0.
-Proof.
-  induction n; simpl; auto with arith.
-Qed.
+Notation minus_diag := Nat.sub_diag (compat "8.4"). (* n - n = 0 *)
 
-Lemma minus_diag_reverse : forall n, 0 = n - n.
+Lemma minus_diag_reverse n : 0 = n - n.
 Proof.
-  auto using minus_diag.
+ symmetry. apply Nat.sub_diag.
 Qed.
-Hint Resolve minus_diag_reverse: arith v62.
 
 Notation minus_n_n := minus_diag_reverse.
 
 (** * Simplification *)
 
-Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
+Lemma minus_plus_simpl_l_reverse n m p : n - m = p + n - (p + m).
 Proof.
-  induction p; simpl; auto with arith.
+ now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub.
 Qed.
-Hint Resolve minus_plus_simpl_l_reverse: arith v62.
 
 (** * Relation with plus *)
 
-Lemma plus_minus : forall n m p, n = m + p -> p = n - m.
+Lemma plus_minus n m p : n = m + p -> p = n - m.
 Proof.
-  intros n m p; pattern m, n; apply nat_double_ind; simpl;
-    intros.
-  replace (n0 - 0) with n0; auto with arith.
-  absurd (0 = S (n0 + p)); auto with arith.
-  auto with arith.
+ symmetry. now apply Nat.add_sub_eq_l.
 Qed.
-Hint Immediate plus_minus: arith v62.
 
-Lemma minus_plus : forall n m, n + m - n = m.
-  symmetry ; auto with arith.
+Lemma minus_plus n m : n + m - n = m.
+Proof.
+ rewrite Nat.add_comm. apply Nat.add_sub.
 Qed.
-Hint Resolve minus_plus: arith v62.
 
-Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n).
+Lemma le_plus_minus_r n m : n <= m -> n + (m - n) = m.
 Proof.
-  intros n m Le; pattern n, m; apply le_elim_rel; simpl;
-    auto with arith.
+ rewrite Nat.add_comm. apply Nat.sub_add.
 Qed.
-Hint Resolve le_plus_minus: arith v62.
 
-Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m.
+Lemma le_plus_minus n m : n <= m -> m = n + (m - n).
 Proof.
-  symmetry ; auto with arith.
+ intros. symmetry. rewrite Nat.add_comm. now apply Nat.sub_add.
 Qed.
-Hint Resolve le_plus_minus_r: arith v62.
 
 (** * Relation with order *)
 
-Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p.
-Proof.
-  intros n m p; generalize n m; clear n m; induction p as [|p HI].
-    intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial.
-
-    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith.
-    intros q r H _. simpl. auto using HI.
-Qed.
-
-Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n.
-Proof.
-  intros n m p; generalize n m; clear n m; induction p as [|p HI].
-    trivial.
+Notation minus_le_compat_r :=
+  Nat.sub_le_mono_r (compat "8.4"). (* n <= m -> n - p <= m - p. *)
 
-    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
-      intros q; destruct q; auto with arith.
-        simpl.
-        apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
-          auto with arith.
+Notation minus_le_compat_l :=
+  Nat.sub_le_mono_l (compat "8.4"). (* n <= m -> p - m <= p - n. *)
 
-      intros q r Hqr _. simpl. auto using HI.
-Qed.
+Notation le_minus := Nat.le_sub_l (compat "8.4"). (* n - m <= n *)
+Notation lt_minus := Nat.sub_lt (compat "8.4"). (* m <= n -> 0 < m -> n-m < n *)
 
-Corollary le_minus : forall n m, n - m <= n.
+Lemma lt_O_minus_lt n m : 0 < n - m -> m < n.
 Proof.
-  intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
+ apply Nat.lt_add_lt_sub_r.
 Qed.
 
-Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
+Theorem not_le_minus_0 n m : ~ m <= n -> n - m = 0.
 Proof.
-  intros n m Le; pattern m, n; apply le_elim_rel; simpl;
-    auto using le_minus with arith.
-    intros; absurd (0 < 0); auto with arith.
+ intros. now apply Nat.sub_0_le, Nat.lt_le_incl, Nat.lt_nge.
 Qed.
-Hint Resolve lt_minus: arith v62.
 
-Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n.
-Proof.
-  intros n m; pattern n, m; apply nat_double_ind; simpl;
-    auto with arith.
-  intros; absurd (0 < 0); trivial with arith.
-Qed.
-Hint Immediate lt_O_minus_lt: arith v62.
+(** * Hints *)
 
-Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0.
-Proof.
-  intros y x; pattern y, x; apply nat_double_ind;
-    [ simpl; trivial with arith
-      | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ]
-      | simpl; intros n m H1 H2; apply H1; unfold not; intros H3;
-	apply H2; apply le_n_S; assumption ].
-Qed.
+Hint Resolve minus_n_O: arith v62.
+Hint Resolve minus_Sn_m: arith v62.
+Hint Resolve minus_diag_reverse: arith v62.
+Hint Resolve minus_plus_simpl_l_reverse: arith v62.
+Hint Immediate plus_minus: arith v62.
+Hint Resolve minus_plus: arith v62.
+Hint Resolve le_plus_minus: arith v62.
+Hint Resolve le_plus_minus_r: arith v62.
+Hint Resolve lt_minus: arith v62.
+Hint Immediate lt_O_minus_lt: arith v62.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index cbb9b376b..d53a1646a 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -6,215 +6,139 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export Plus.
-Require Export Minus.
-Require Export Lt.
-Require Export Le.
+(** * Properties of multiplication.
 
-Local Open Scope nat_scope.
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [Nat.mul] is defined in [Init/Nat.v].
+*)
 
-Implicit Types m n p : nat.
+Require Import PeanoNat.
+(** For Compatibility: *)
+Require Export Plus Minus Le Lt.
 
-(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *)
+Local Open Scope nat_scope.
 
 (** * [nat] is a semi-ring *)
 
 (** ** Zero property *)
 
-Lemma mult_0_r : forall n, n * 0 = 0.
-Proof.
-  intro; symmetry ; apply mult_n_O.
-Qed.
-
-Lemma mult_0_l : forall n, 0 * n = 0.
-Proof.
-  reflexivity.
-Qed.
+Notation mult_0_l := Nat.mul_0_l (compat "8.4"). (* 0 * n = 0 *)
+Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *)
 
 (** ** 1 is neutral *)
 
-Lemma mult_1_l : forall n, 1 * n = n.
-Proof.
-  simpl; auto with arith.
-Qed.
-Hint Resolve mult_1_l: arith v62.
+Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *)
+Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *)
 
-Lemma mult_1_r : forall n, n * 1 = n.
-Proof.
-  induction n; [ trivial |
-    simpl; rewrite IHn; reflexivity].
-Qed.
-Hint Resolve mult_1_r: arith v62.
+Hint Resolve mult_1_l mult_1_r: arith v62.
 
 (** ** Commutativity *)
 
-Lemma mult_comm : forall n m, n * m = m * n.
-Proof.
-intros; induction n; simpl; auto with arith.
-rewrite <- mult_n_Sm.
-rewrite IHn; apply plus_comm.
-Qed.
+Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *)
+
 Hint Resolve mult_comm: arith v62.
 
 (** ** Distributivity *)
 
-Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
-Proof.
-  intros; induction n; simpl; auto with arith.
-  rewrite <- plus_assoc, IHn; auto with arith.
-Qed.
-Hint Resolve mult_plus_distr_r: arith v62.
+Notation mult_plus_distr_r :=
+  Nat.mul_add_distr_r (compat "8.4"). (* (n+m)*p = n*p + m*p *)
 
-Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
-Proof.
-  induction n. trivial.
-  intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4.
-Qed.
+Notation mult_plus_distr_l :=
+  Nat.mul_add_distr_l (compat "8.4"). (* n*(m+p) = n*m + n*p *)
 
-Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
-Proof.
-  intros; induction n, m using nat_double_ind; simpl; auto with arith.
-  rewrite <- minus_plus_simpl_l_reverse; auto with arith.
-Qed.
-Hint Resolve mult_minus_distr_r: arith v62.
+Notation mult_minus_distr_r :=
+  Nat.mul_sub_distr_r (compat "8.4"). (* (n-m)*p = n*p - m*p *)
 
-Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p.
-Proof.
-  intros n m p.
-  rewrite mult_comm, mult_minus_distr_r, (mult_comm m n), (mult_comm p n); reflexivity.
-Qed.
+Notation mult_minus_distr_l :=
+  Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *)
+
+Hint Resolve mult_plus_distr_r: arith v62.
+Hint Resolve mult_minus_distr_r: arith v62.
 Hint Resolve mult_minus_distr_l: arith v62.
 
 (** ** Associativity *)
 
-Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
-Proof.
-  intros; induction n; simpl; auto with arith.
-  rewrite mult_plus_distr_r.
-  induction IHn; auto with arith.
-Qed.
-Hint Resolve mult_assoc_reverse: arith v62.
+Notation mult_assoc := Nat.mul_assoc (compat "8.4"). (* n*(m*p)=n*m*p *)
 
-Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
+Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p).
 Proof.
-  auto with arith.
+ symmetry. apply Nat.mul_assoc.
 Qed.
+
+Hint Resolve mult_assoc_reverse: arith v62.
 Hint Resolve mult_assoc: arith v62.
 
 (** ** Inversion lemmas *)
 
-Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+Lemma mult_is_O n m : n * m = 0 -> n = 0 \/ m = 0.
 Proof.
-  destruct n as [| n]; simpl; intros m H.
-    left; trivial.
-    right; apply plus_is_O in H; destruct H; trivial.
+ apply Nat.eq_mul_0.
 Qed.
 
-Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
+Lemma mult_is_one n m : n * m = 1 -> n = 1 /\ m = 1.
 Proof.
-  destruct n as [|n]; simpl; intros m H.
-    edestruct O_S; eauto.
-    destruct plus_is_one with (1:=H) as [[-> Hnm] | [-> Hnm]].
-      simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
-      rewrite mult_1_r in Hnm; auto.
+ apply Nat.eq_mul_1.
 Qed.
 
 (** ** Multiplication and successor *)
 
-Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
-Proof.
-  intros; simpl. rewrite plus_comm. reflexivity.
-Qed.
-
-Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.
-Proof.
-  induction n as [| p H]; intro m; simpl.
-  reflexivity.
-  rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity.
-Qed.
+Notation mult_succ_l := Nat.mul_succ_l (compat "8.4"). (* S n * m = n * m + m *)
+Notation mult_succ_r := Nat.mul_succ_r (compat "8.4"). (* n * S m = n * m + n *)
 
 (** * Compatibility with orders *)
 
-Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
+Lemma mult_O_le n m : m = 0 \/ n <= m * n.
 Proof.
-  induction m; simpl; auto with arith.
+ destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
 Qed.
 Hint Resolve mult_O_le: arith v62.
 
-Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
+Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.
 Proof.
-  induction p as [| p IHp]; intros; simpl.
-  apply le_n.
-  auto using plus_le_compat.
+ apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *)
 Qed.
 Hint Resolve mult_le_compat_l: arith.
 
-
-Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
+Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p.
 Proof.
-  intros m n p H; rewrite mult_comm, (mult_comm n); auto with arith.
+ apply Nat.mul_le_mono_nonneg_r, Nat.le_0_l.
 Qed.
 
-Lemma mult_le_compat :
-  forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q.
+Lemma mult_le_compat n m p q : n <= m -> p <= q -> n * p <= m * q.
 Proof.
-  intros m n p q Hmn Hpq; induction Hmn.
-  induction Hpq.
-  (* m*p<=m*p *)
-  apply le_n.
-  (* m*p<=m*m0 -> m*p<=m*(S m0) *)
-  rewrite <- mult_n_Sm; apply le_trans with (m * m0).
-  assumption.
-  apply le_plus_l.
-  (* m*p<=m0*q -> m*p<=(S m0)*q *)
-  simpl; apply le_trans with (m0 * q).
-  assumption.
-  apply le_plus_r.
+  intros. apply Nat.mul_le_mono_nonneg; trivial; apply Nat.le_0_l.
 Qed.
 
-Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
+Lemma mult_S_lt_compat_l n m p : m < p -> S n * m < S n * p.
 Proof.
-  induction n; intros; simpl in *.
-    rewrite <- 2 plus_n_O; assumption.
-    auto using plus_lt_compat.
+  apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ.
 Qed.
 
 Hint Resolve mult_S_lt_compat_l: arith.
 
-Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m.
+Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m.
 Proof.
- intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
- now apply mult_S_lt_compat_l.
+ intros. now apply Nat.mul_lt_mono_pos_l.
 Qed.
 
-Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
+Lemma mult_lt_compat_r n m p : n < m -> 0 < p -> n * p < m * p.
 Proof.
-  intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
-  rewrite (mult_comm m), (mult_comm n). now apply mult_S_lt_compat_l.
+ intros. now apply Nat.mul_lt_mono_pos_r.
 Qed.
 
-Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
+Lemma mult_S_le_reg_l n m p : S n * m <= S n * p -> m <= p.
 Proof.
-  intros m n p H; destruct (le_or_lt n p). trivial.
-  assert (H1:S m * n < S m * n).
-    apply le_lt_trans with (m := S m * p). assumption.
-    apply mult_S_lt_compat_l. assumption.
-  elim (lt_irrefl _ H1).
+ apply Nat.mul_le_mono_pos_l, Nat.lt_0_succ.
 Qed.
 
 (** * n|->2*n and n|->2n+1 have disjoint image *)
 
-Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.
+Theorem odd_even_lem p q : 2 * p + 1 <> 2 * q.
 Proof.
-  induction p; destruct q.
-    discriminate.
-    simpl; rewrite plus_comm. discriminate.
-    discriminate.
-    intro H0; destruct (IHp q).
-    replace (2 * q) with (2 * S q - 2).
-      rewrite <- H0; simpl.
-      repeat rewrite (fun x y => plus_comm x (S y)); simpl;  auto.
-    simpl; rewrite (fun y => plus_comm q (S y)); destruct q; simpl; auto.
+ intro. apply (Nat.Even_Odd_False (2*q)).
+ - now exists q.
+ - now exists p.
 Qed.
 
 
@@ -232,10 +156,9 @@ Fixpoint mult_acc (s:nat) m n : nat :=
 
 Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 Proof.
-  induction n as [| p IHp]; simpl; auto.
-  intros s m; rewrite <- plus_tail_plus; rewrite <- IHp.
-  rewrite <- plus_assoc_reverse; apply f_equal2; auto.
-  rewrite plus_comm; auto.
+  induction n as [| n IHn]; simpl; auto.
+  intros. rewrite Nat.add_assoc, IHn. f_equal.
+  rewrite Nat.add_comm. apply plus_tail_plus.
 Qed.
 
 Definition tail_mult n m := mult_acc 0 m n.
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
new file mode 100644
index 000000000..3657d9544
--- /dev/null
+++ b/theories/Arith/PeanoNat.v
@@ -0,0 +1,755 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+Require Import NAxioms NProperties OrdersFacts.
+
+(** Implementation of [NAxiomsSig] by [nat] *)
+
+Module Nat
+ <: NAxiomsSig
+ <: UsualDecidableTypeFull
+ <: OrderedTypeFull
+ <: TotalOrder.
+
+(** Operations over [nat] are defined in a separate module *)
+
+Include Coq.Init.Nat.
+
+(** When including property functors, inline t eq zero one two lt le succ *)
+
+Set Inline Level 50.
+
+(** All operations are well-defined (trivial here since eq is Leibniz) *)
+
+Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
+Local Obligation Tactic := simpl_relation.
+Program Instance succ_wd : Proper (eq==>eq) S.
+Program Instance pred_wd : Proper (eq==>eq) pred.
+Program Instance add_wd : Proper (eq==>eq==>eq) plus.
+Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
+Program Instance mul_wd : Proper (eq==>eq==>eq) mult.
+Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
+Program Instance div_wd : Proper (eq==>eq==>eq) div.
+Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
+Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit.
+
+(** Bi-directional induction. *)
+
+Theorem bi_induction :
+  forall A : nat -> Prop, Proper (eq==>iff) A ->
+    A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
+Proof.
+intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
+Qed.
+
+(** Recursion fonction *)
+
+Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A :=
+  nat_rect (fun _ => A).
+
+Instance recursion_wd {A} (Aeq : relation A) :
+ Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.
+Proof.
+intros a a' Ha f f' Hf n n' Hn. subst n'.
+induction n; simpl; auto. apply Hf; auto.
+Qed.
+
+Theorem recursion_0 :
+  forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a.
+Proof.
+reflexivity.
+Qed.
+
+Theorem recursion_succ :
+  forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A),
+    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
+      forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
+Proof.
+unfold Proper, respectful in *; induction n; simpl; auto.
+Qed.
+
+(** ** Remaining constants not defined in Coq.Init.Nat *)
+
+(** NB: Aliasing [le] is mandatory, since only a Definition can implement
+    an interface Parameter... *)
+
+Definition eq := @Logic.eq nat.
+Definition le := Peano.le.
+Definition lt := Peano.lt.
+
+(** ** Basic specifications : pred add sub mul *)
+
+Lemma pred_succ n : pred (S n) = n.
+Proof.
+reflexivity.
+Qed.
+
+Lemma pred_0 : pred 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma one_succ : 1 = S 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma two_succ : 2 = S 1.
+Proof.
+reflexivity.
+Qed.
+
+Lemma add_0_l n : 0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Lemma add_succ_l n m : (S n) + m = S (n + m).
+Proof.
+reflexivity.
+Qed.
+
+Lemma sub_0_r n : n - 0 = n.
+Proof.
+now destruct n.
+Qed.
+
+Lemma sub_succ_r n m : n - (S m) = pred (n - m).
+Proof.
+revert m. induction n; destruct m; simpl; auto. apply sub_0_r.
+Qed.
+
+Lemma mul_0_l n : 0 * n = 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma mul_succ_l n m : S n * m = n * m + m.
+Proof.
+assert (succ_r : forall x y, x+S y = S(x+y)) by now induction x.
+assert (comm : forall x y, x+y = y+x).
+{ induction x; simpl; auto. intros; rewrite succ_r; now f_equal. }
+now rewrite comm.
+Qed.
+
+Lemma lt_succ_r n m : n < S m <-> n <= m.
+Proof.
+split. apply Peano.le_S_n. induction 1; auto.
+Qed.
+
+(** ** Boolean comparisons *)
+
+Lemma eqb_eq n m : eqb n m = true <-> n = m.
+Proof.
+ revert m.
+ induction n; destruct m; simpl; rewrite ?IHn; split; try easy.
+ - now intros ->.
+ - now injection 1.
+Qed.
+
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
+Proof.
+ revert m.
+ induction n; destruct m; simpl.
+ - now split.
+ - split; trivial. intros; apply Peano.le_0_n.
+ - now split.
+ - rewrite IHn; split.
+   + apply Peano.le_n_S.
+   + apply Peano.le_S_n.
+Qed.
+
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
+Proof.
+ apply leb_le.
+Qed.
+
+(** ** Decidability of equality over [nat]. *)
+
+Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.
+Proof.
+  induction n; destruct m.
+  - now left.
+  - now right.
+  - now right.
+  - destruct (IHn m); [left|right]; auto.
+Defined.
+
+(** ** Ternary comparison *)
+
+(** With [nat], it would be easier to prove first [compare_spec],
+    then the properties below. But then we wouldn't be able to
+    benefit from functor [BoolOrderFacts] *)
+
+Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
+Proof.
+ revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy.
+Qed.
+
+Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.
+Proof.
+ revert m; induction n; destruct m; simpl; rewrite ?IHn; split; try easy.
+ - intros _. apply Peano.le_n_S, Peano.le_0_n.
+ - apply Peano.le_n_S.
+ - apply Peano.le_S_n.
+Qed.
+
+Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
+Proof.
+ revert m; induction n; destruct m; simpl; rewrite ?IHn.
+ - now split.
+ - split; intros. apply Peano.le_0_n. easy.
+ - split. now destruct 1. inversion 1.
+ - split; intros. now apply Peano.le_n_S. now apply Peano.le_S_n.
+Qed.
+
+Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
+Proof.
+ revert m; induction n; destruct m; simpl; trivial.
+Qed.
+
+Lemma compare_succ n m : (S n ?= S m) = (n ?= m).
+Proof.
+ reflexivity.
+Qed.
+
+
+(* BUG: Ajout d'un cas * après preuve finie (deuxième niveau +++*** ) :
+    *  --->   Anomaly: Uncaught exception Proofview.IndexOutOfRange(_). Please report. *)
+
+(** ** Minimum, maximum *)
+
+Lemma max_l : forall n m, m <= n -> max n m = n.
+Proof.
+ exact Peano.max_l.
+Qed.
+
+Lemma max_r : forall n m, n <= m -> max n m = m.
+Proof.
+ exact Peano.max_r.
+Qed.
+
+Lemma min_l : forall n m, n <= m -> min n m = n.
+Proof.
+ exact Peano.min_l.
+Qed.
+
+Lemma min_r : forall n m, m <= n -> min n m = m.
+Proof.
+ exact Peano.min_r.
+Qed.
+
+(** Some more advanced properties of comparison and orders,
+    including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *)
+
+Include BoolOrderFacts.
+
+(** 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.
+
+(** ** Power *)
+
+Lemma pow_neg_r a b : b<0 -> a^b = 0. inversion 1. Qed.
+
+Lemma pow_0_r a : a^0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma pow_succ_r a b : 0<=b -> a^(S b) = a * a^b.
+Proof. reflexivity. Qed.
+
+(** ** Square *)
+
+Lemma square_spec n : square n = n * n.
+Proof. reflexivity. Qed.
+
+(** ** Parity *)
+
+Definition Even n := exists m, n = 2*m.
+Definition Odd n := exists m, n = 2*m+1.
+
+Module Private_Parity.
+
+Lemma Even_1 : ~ Even 1.
+Proof.
+ intros ([|], H); try discriminate.
+ simpl in H. now rewrite <- plus_n_Sm in H.
+Qed.
+
+Lemma Even_2 n : Even n <-> Even (S (S n)).
+Proof.
+ split; intros (m,H).
+ - exists (S m). rewrite H. simpl. now rewrite plus_n_Sm.
+ - destruct m; try discriminate.
+   exists m. simpl in H. rewrite <- plus_n_Sm in H. now inversion H.
+Qed.
+
+Lemma Odd_0 : ~ Odd 0.
+Proof.
+ now intros ([|], H).
+Qed.
+
+Lemma Odd_2 n : Odd n <-> Odd (S (S n)).
+Proof.
+ split; intros (m,H).
+ - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m).
+ - destruct m; try discriminate.
+   exists m. simpl in H. rewrite <- plus_n_Sm in H. inversion H.
+   simpl. now rewrite <- !plus_n_Sm, <- !plus_n_O.
+Qed.
+
+End Private_Parity.
+Import Private_Parity.
+
+Lemma even_spec : forall n, even n = true <-> Even n.
+Proof.
+ fix 1.
+  destruct n as [|[|n]]; simpl.
+  - split; [ now exists 0 | trivial ].
+  - split; [ discriminate | intro H; elim (Even_1 H) ].
+  - rewrite even_spec. apply Even_2.
+Qed.
+
+Lemma odd_spec : forall n, odd n = true <-> Odd n.
+Proof.
+ unfold odd.
+ fix 1.
+  destruct n as [|[|n]]; simpl.
+  - split; [ discriminate | intro H; elim (Odd_0 H) ].
+  - split; [ now exists 0 | trivial ].
+  - rewrite odd_spec. apply Odd_2.
+Qed.
+
+(** ** Division *)
+
+Lemma divmod_spec : forall x y q u, u <= y ->
+ let (q',u') := divmod x y q u in
+ x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.
+Proof.
+ induction x.
+ - simpl; intuition.
+ - intros y q u H. destruct u; simpl divmod.
+   + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u').
+     intros (EQ,LE); split; trivial.
+     rewrite <- EQ, sub_0_r, sub_diag, add_0_r.
+     now rewrite !add_succ_l, <- add_succ_r, <- add_assoc, mul_succ_r.
+   + assert (H' : u <= y).
+     { apply le_trans with (S u); trivial. do 2 constructor. }
+     generalize (IHx y q u H'). destruct divmod as (q',u').
+     intros (EQ,LE); split; trivial.
+     rewrite <- EQ.
+     rewrite !add_succ_l, <- add_succ_r. f_equal. now rewrite <- sub_succ_l.
+Qed.
+
+Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y.
+Proof.
+ intros Hy.
+ destruct y; [ now elim Hy | clear Hy ].
+ unfold div, modulo.
+ generalize (divmod_spec x y 0 y (le_n y)).
+ destruct divmod as (q,u).
+ intros (U,V).
+ simpl in *.
+ now rewrite mul_0_r, sub_diag, !add_0_r in U.
+Qed.
+
+Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y.
+Proof.
+ intros Hx Hy. split. apply le_0_l.
+ destruct y; [ now elim Hy | clear Hy ].
+ unfold modulo.
+ apply lt_succ_r, le_sub_l.
+Qed.
+
+(** ** Square root *)
+
+Lemma sqrt_iter_spec : forall k p q r,
+ q = p+p -> r<=q ->
+ let s := sqrt_iter k p q r in
+ s*s <= k + p*p + (q - r) < (S s)*(S s).
+Proof.
+ induction k.
+ - (* k = 0 *)
+   simpl; intros p q r Hq Hr.
+   split.
+   + apply le_add_r.
+   + apply lt_succ_r.
+     rewrite mul_succ_r.
+     rewrite add_assoc, (add_comm p), <- add_assoc.
+     apply add_le_mono_l.
+     rewrite <- Hq. apply le_sub_l.
+ - (* k = S k' *)
+   destruct r.
+   + (* r = 0 *)
+     intros Hq _.
+     replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))).
+     * apply IHk.
+       simpl. now rewrite add_succ_r, Hq. apply le_n.
+     * rewrite sub_diag, sub_0_r, add_0_r. simpl.
+       rewrite add_succ_r; f_equal. rewrite <- add_assoc; f_equal.
+       rewrite mul_succ_r, (add_comm p), <- add_assoc. now f_equal.
+   + (* r = S r' *)
+     intros Hq Hr.
+     replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)).
+     * apply IHk; trivial. apply le_trans with (S r); trivial. do 2 constructor.
+     * simpl. rewrite <- add_succ_r. f_equal. rewrite <- sub_succ_l; trivial.
+Qed.
+
+Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).
+Proof.
+ set (s:=sqrt n).
+ replace n with (n + 0*0 + (0-0)).
+ apply sqrt_iter_spec; auto.
+ simpl. now rewrite !add_0_r.
+Qed.
+
+Definition sqrt_spec a (Ha:0<=a) := sqrt_specif a.
+
+Lemma sqrt_neg a : a<0 -> sqrt a = 0.
+Proof. inversion 1. Qed.
+
+(** ** Logarithm *)
+
+Lemma log2_iter_spec : forall k p q r,
+ 2^(S p) = q + S r -> r < 2^p ->
+ let s := log2_iter k p q r in
+ 2^s <= k + q < 2^(S s).
+Proof.
+ induction k.
+ - (* k = 0 *)
+   intros p q r EQ LT. simpl log2_iter. cbv zeta.
+   split.
+   + rewrite add_0_l.
+     rewrite (add_le_mono_l _ _ (2^p)).
+     simpl pow in EQ. rewrite add_0_r in EQ. rewrite EQ.
+     rewrite add_comm. apply add_le_mono_r. apply LT.
+   + rewrite EQ, add_comm. apply add_lt_mono_l.
+     apply lt_succ_r, le_0_l.
+ - (* k = S k' *)
+   intros p q r EQ LT. destruct r.
+   + (* r = 0 *)
+     rewrite add_succ_r, add_0_r in EQ.
+     rewrite add_succ_l, <- add_succ_r. apply IHk.
+     * rewrite <- EQ. remember (S p) as p'; simpl. now rewrite add_0_r.
+     * rewrite EQ. constructor.
+   + (* r = S r' *)
+     rewrite add_succ_l, <- add_succ_r. apply IHk.
+     * now rewrite add_succ_l, <- add_succ_r.
+     * apply le_lt_trans with (S r); trivial. do 2 constructor.
+Qed.
+
+Lemma log2_spec n : 0<n ->
+ 2^(log2 n) <= n < 2^(S (log2 n)).
+Proof.
+ intros.
+ set (s:=log2 n).
+ replace n with (pred n + 1).
+ apply log2_iter_spec; auto.
+ rewrite add_1_r.
+ apply succ_pred. now apply neq_sym, lt_neq.
+Qed.
+
+Lemma log2_nonpos n : n<=0 -> log2 n = 0.
+Proof.
+ inversion 1; now subst.
+Qed.
+
+(** ** Gcd *)
+
+Definition divide x y := exists z, y=z*x.
+Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.
+
+Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
+Proof.
+ fix 1.
+ intros [|a] b; simpl.
+ split.
+  now exists 0.
+  exists 1. simpl. now rewrite <- plus_n_O.
+ fold (b mod (S a)).
+ destruct (gcd_divide (b mod (S a)) (S a)) as (H,H').
+ set (a':=S a) in *.
+ split; auto.
+ rewrite (div_mod b a') at 2 by discriminate.
+ destruct H as (u,Hu), H' as (v,Hv).
+ rewrite mul_comm.
+ exists ((b/a')*v + u).
+ rewrite mul_add_distr_r.
+ now rewrite <- mul_assoc, <- Hv, <- Hu.
+Qed.
+
+Lemma gcd_divide_l : forall a b, (gcd a b | a).
+Proof.
+ intros. apply gcd_divide.
+Qed.
+
+Lemma gcd_divide_r : forall a b, (gcd a b | b).
+Proof.
+ intros. apply gcd_divide.
+Qed.
+
+Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
+Proof.
+ fix 1.
+ intros [|a] b; simpl; auto.
+ fold (b mod (S a)).
+ intros c H H'. apply gcd_greatest; auto.
+ set (a':=S a) in *.
+ rewrite (div_mod b a') in H' by discriminate.
+ destruct H as (u,Hu), H' as (v,Hv).
+ exists (v - (b/a')*u).
+ rewrite mul_comm in Hv.
+ rewrite mul_sub_distr_r, <- Hv, <- mul_assoc, <-Hu.
+ now rewrite add_comm, add_sub.
+Qed.
+
+Lemma gcd_nonneg a b : 0<=gcd a b.
+Proof. apply le_0_l. Qed.
+
+
+(** ** Bitwise operations *)
+
+Lemma div2_double n : div2 (2*n) = n.
+Proof.
+ induction n; trivial.
+ simpl mul. rewrite add_succ_r. simpl. now f_equal.
+Qed.
+
+Lemma div2_succ_double n : div2 (S (2*n)) = n.
+Proof.
+ induction n; trivial.
+ simpl. f_equal. now rewrite add_succ_r.
+Qed.
+
+Lemma le_div2 n : div2 (S n) <= n.
+Proof.
+ revert n.
+ fix 1.
+ destruct n; simpl; trivial. apply lt_succ_r.
+ destruct n; [simpl|]; trivial. now constructor.
+Qed.
+
+Lemma lt_div2 n : 0 < n -> div2 n < n.
+Proof.
+ destruct n.
+ - inversion 1.
+ - intros _. apply lt_succ_r, le_div2.
+Qed.
+
+Lemma div2_decr a n : a <= S n -> div2 a <= n.
+Proof.
+ destruct a; intros H.
+ - simpl. apply le_0_l.
+ - apply succ_le_mono in H.
+   apply le_trans with a; [ apply le_div2 | trivial ].
+Qed.
+
+Lemma double_twice : forall n, double n = 2*n.
+Proof.
+ simpl; intros. now rewrite add_0_r.
+Qed.
+
+Lemma testbit_0_l : forall n, testbit 0 n = false.
+Proof.
+ now induction n.
+Qed.
+
+Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
+Proof.
+ unfold testbit. rewrite odd_spec. now exists a.
+Qed.
+
+Lemma testbit_even_0 a : testbit (2*a) 0 = false.
+Proof.
+ unfold testbit, odd. rewrite (proj2 (even_spec _)); trivial.
+ now exists a.
+Qed.
+
+Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n.
+Proof.
+ unfold testbit; fold testbit.
+ rewrite add_1_r. f_equal.
+ apply div2_succ_double.
+Qed.
+
+Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n.
+Proof.
+ unfold testbit; fold testbit. f_equal. apply div2_double.
+Qed.
+
+Lemma shiftr_specif : forall a n m,
+ testbit (shiftr a n) m = testbit a (m+n).
+Proof.
+ induction n; intros m. trivial.
+ now rewrite add_0_r.
+ now rewrite add_succ_r, <- add_succ_l, <- IHn.
+Qed.
+
+Lemma shiftl_specif_high : forall a n m, n<=m ->
+ testbit (shiftl a n) m = testbit a (m-n).
+Proof.
+ induction n; intros m H. trivial.
+ now rewrite sub_0_r.
+ destruct m. inversion H.
+ simpl. apply succ_le_mono in H.
+ change (shiftl a (S n)) with (double (shiftl a n)).
+ rewrite double_twice, div2_double. now apply IHn.
+Qed.
+
+Lemma shiftl_spec_low : forall a n m, m<n ->
+ testbit (shiftl a n) m = false.
+Proof.
+ induction n; intros m H. inversion H.
+ change (shiftl a (S n)) with (double (shiftl a n)).
+ destruct m; simpl.
+ unfold odd. apply negb_false_iff.
+ apply even_spec. exists (shiftl a n). apply double_twice.
+ rewrite double_twice, div2_double. apply IHn.
+ now apply succ_le_mono.
+Qed.
+
+Lemma div2_bitwise : forall op n a b,
+ div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
+Proof.
+ intros. unfold bitwise; fold bitwise.
+ destruct (op (odd a) (odd b)).
+ now rewrite div2_succ_double.
+ now rewrite add_0_l, div2_double.
+Qed.
+
+Lemma odd_bitwise : forall op n a b,
+ odd (bitwise op (S n) a b) = op (odd a) (odd b).
+Proof.
+ intros. unfold bitwise; fold bitwise.
+ destruct (op (odd a) (odd b)).
+ apply odd_spec. rewrite add_comm. eexists; eauto.
+ unfold odd. apply negb_false_iff. apply even_spec.
+ rewrite add_0_l; eexists; eauto.
+Qed.
+
+Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) ->
+ forall n m a b, a<=n ->
+ testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
+Proof.
+ intros op Hop.
+ induction n; intros m a b Ha.
+ simpl. inversion Ha; subst. now rewrite testbit_0_l.
+ destruct m.
+ apply odd_bitwise.
+ unfold testbit; fold testbit. rewrite div2_bitwise.
+ apply IHn. now apply div2_decr.
+Qed.
+
+Lemma testbit_bitwise_2 : forall op, op false false = false ->
+ forall n m a b, a<=n -> b<=n ->
+ testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
+Proof.
+ intros op Hop.
+ induction n; intros m a b Ha Hb.
+ simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l.
+ destruct m.
+ apply odd_bitwise.
+ unfold testbit; fold testbit. rewrite div2_bitwise.
+ apply IHn; now apply div2_decr.
+Qed.
+
+Lemma land_spec a b n :
+ testbit (land a b) n = testbit a n && testbit b n.
+Proof.
+ unfold land. apply testbit_bitwise_1; trivial.
+Qed.
+
+Lemma ldiff_spec a b n :
+ testbit (ldiff a b) n = testbit a n && negb (testbit b n).
+Proof.
+ unfold ldiff. apply testbit_bitwise_1; trivial.
+Qed.
+
+Lemma lor_spec a b n :
+ testbit (lor a b) n = testbit a n || testbit b n.
+Proof.
+ unfold lor. apply testbit_bitwise_2.
+ - trivial.
+ - destruct (compare_spec a b).
+   + rewrite max_l; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+ - destruct (compare_spec a b).
+   + rewrite max_r; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+Qed.
+
+Lemma lxor_spec a b n :
+ testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
+Proof.
+ unfold lxor. apply testbit_bitwise_2.
+ - trivial.
+ - destruct (compare_spec a b).
+   + rewrite max_l; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+ - destruct (compare_spec a b).
+   + rewrite max_r; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+Qed.
+
+Lemma div2_spec a : div2 a = shiftr a 1.
+Proof.
+ reflexivity.
+Qed.
+
+(** Aliases with extra dummy hypothesis, to fulfil the interface *)
+
+Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ' a n.
+Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ' a n.
+Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.
+Proof. inversion H. Qed.
+
+Definition shiftl_spec_high a n m (_:0<=m) := shiftl_specif_high a n m.
+Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m.
+
+(** Properties of advanced functions (pow, sqrt, log2, ...) *)
+
+Include NExtraProp.
+
+End Nat.
+
+(** Re-export notations that should be available even when
+    the [Nat] module is not imported. *)
+
+Bind Scope nat_scope with Nat.t nat.
+
+Infix "^" := Nat.pow : nat_scope.
+Infix "=?" := Nat.eqb (at level 70) : nat_scope.
+Infix "<=?" := Nat.leb (at level 70) : nat_scope.
+Infix "<?" := Nat.ltb (at level 70) : nat_scope.
+Infix "?=" := Nat.compare (at level 70) : nat_scope.
+Infix "/" := Nat.div : nat_scope.
+Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
+
+Hint Unfold Nat.le : core.
+Hint Unfold Nat.lt : core.
+
+(** [Nat] contains an [order] tactic for natural numbers *)
+
+(** Note that [Nat.order] is domain-agnostic: it will not prove
+    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
+
+Section TestOrder.
+ Let test : forall x y, x<=y -> y<=x -> x=y.
+ Proof.
+ Nat.order.
+ Qed.
+End TestOrder.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 9b8ebfe55..72edc6eef 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,47 +6,61 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Decidable.
+Require Import Decidable PeanoNat.
 Require Eqdep_dec.
-Require Import Le Lt.
 Local Open Scope nat_scope.
 
 Implicit Types m n x y : nat.
 
-Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}.
+Theorem O_or_S n : {m : nat | S m = n} + {0 = n}.
 Proof.
   induction n.
-  auto.
-  left; exists n; auto.
+  - now right.
+  - left; exists n; auto.
 Defined.
 
-Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
-Proof.
-  induction n; destruct m; auto.
-  elim (IHn m); auto.
-Defined.
+Notation eq_nat_dec := Nat.eq_dec (compat "8.4").
 
 Hint Resolve O_or_S eq_nat_dec: arith.
 
-Theorem dec_eq_nat : forall n m, decidable (n = m).
-  intros x y; unfold decidable; elim (eq_nat_dec x y); auto with arith.
+Theorem dec_eq_nat n m : decidable (n = m).
+Proof.
+  elim (Nat.eq_dec n m); [left|right]; trivial.
 Defined.
 
-Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec.
+Definition UIP_nat:= Eqdep_dec.UIP_dec Nat.eq_dec.
+
+Import EqNotations.
 
 Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2.
 Proof.
 fix 3.
-refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh
-  with le_n _ => _ |le_S _ i H => _ end).
-refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, 
-  le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with
-    |le_n _ => fun eq => _ |le_S _ j H' => fun eq => _ end eq_refl).
-rewrite (UIP_nat _ _ eq eq_refl). reflexivity.
-subst m. destruct (Lt.lt_irrefl j H').
-refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop
-  with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h'
-    with |le_n _ => _ |le_S _ j H2 => fun H' => _ end H).
-destruct m. exact I. intros; destruct (Lt.lt_irrefl m H').
-f_equal. apply le_unique.
+destruct h1 as [ | i h1 ]; intros h2.
+- set (Return k (le:m<=k) :=
+       forall (eq:m=k),
+         le_n m = (rew eq in fun (le':m<=m) => le') le).
+  refine
+     (match h2 as h2' return (Return _ h2') with
+        | le_n _ => fun eq => _
+        | le_S _ j h2 => fun eq => _
+      end eq_refl).
+  + rewrite (UIP_nat _ _ eq eq_refl). simpl. reflexivity.
+  + exfalso. revert h2. rewrite eq. apply Nat.lt_irrefl.
+- set (Return k (le:m<=k) :=
+       match k as k' return (m <= k' -> Prop) with
+         | 0 => fun _ => True
+         | S i' => fun (le':m<=S i') => forall (H':m<=i'), le_S _ _ H' = le'
+       end le).
+  refine
+    (match h2 as h2' return (Return _ h2') with
+       | le_n _ => _
+       | le_S _ j h2 => fun h1' => _
+     end h1).
+  + unfold Return; clear. destruct m; simpl.
+    * exact I.
+    * intros h1'. destruct (Nat.lt_irrefl _ h1').
+  + f_equal. apply le_unique.
 Qed.
+
+(** For compatibility *)
+Require Import Le Lt.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 5428ada32..3b823da6f 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,176 +6,139 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Properties of addition. [add] is defined in [Init/Peano.v] as:
+(** Properties of addition.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [Nat.add] is defined in [Init/Nat.v] as:
 <<
-Fixpoint plus (n m:nat) : nat :=
+Fixpoint add (n m:nat) : nat :=
   match n with
   | O => m
   | S p => S (p + m)
   end
-where "n + m" := (plus n m) : nat_scope.
+where "n + m" := (add n m) : nat_scope.
 >>
- *)
+*)
 
-Require Import Le.
-Require Import Lt.
+Require Import PeanoNat.
 
 Local Open Scope nat_scope.
 
-Implicit Types m n p q : nat.
-
-(** * Zero is neutral 
-Deprecated : Already in Init/Peano.v *)
-Notation plus_0_l := plus_O_n (only parsing).
-Definition plus_0_r n := eq_sym (plus_n_O n).
-
-(** * Commutativity *)
-
-Lemma plus_comm : forall n m, n + m = m + n.
-Proof.
-  intros n m; elim n; simpl; auto with arith.
-  intros y H; elim (plus_n_Sm m y); auto with arith.
-Qed.
-Hint Immediate plus_comm: arith v62.
-
-(** * Associativity *)
+(** * Neutrality of 0, commutativity, associativity *)
 
-Definition plus_Snm_nSm : forall n m, S n + m = n + S m:=
- plus_n_Sm.
+Notation plus_0_l := Nat.add_0_l (compat "8.4").
+Notation plus_0_r := Nat.add_0_r (compat "8.4").
+Notation plus_comm := Nat.add_comm (compat "8.4").
+Notation plus_assoc := Nat.add_assoc (compat "8.4").
 
-Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
-Proof.
-  intros n m p; elim n; simpl; auto with arith.
-Qed.
-Hint Resolve plus_assoc: arith v62.
+Notation plus_permute := Nat.add_shuffle3 (compat "8.4").
 
-Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p).
-Proof.
-  intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith.
-Qed.
+Definition plus_Snm_nSm : forall n m, S n + m = n + S m :=
+ Peano.plus_n_Sm.
 
-Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p).
+Lemma plus_assoc_reverse n m p : n + m + p = n + (m + p).
 Proof.
-  auto with arith.
+  symmetry. apply Nat.add_assoc.
 Qed.
-Hint Resolve plus_assoc_reverse: arith v62.
 
 (** * Simplification *)
 
-Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.
+Lemma plus_reg_l n m p : p + n = p + m -> n = m.
 Proof.
-  intros m p n; induction n; simpl; auto with arith.
+ apply Nat.add_cancel_l.
 Qed.
 
-Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
+Lemma plus_le_reg_l n m p : p + n <= p + m -> n <= m.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_le_mono_l.
 Qed.
 
-Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
+Lemma plus_lt_reg_l n m p : p + n < p + m -> n < m.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
 
 (** * Compatibility with order *)
 
-Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.
+Lemma plus_le_compat_l n m p : n <= m -> p + n <= p + m.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_le_mono_l.
 Qed.
-Hint Resolve plus_le_compat_l: arith v62.
 
-Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p.
+Lemma plus_le_compat_r n m p : n <= m -> n + p <= m + p.
 Proof.
-  induction 1; simpl; auto with arith.
+ apply Nat.add_le_mono_r.
 Qed.
-Hint Resolve plus_le_compat_r: arith v62.
 
-Lemma le_plus_l : forall n m, n <= n + m.
+Lemma plus_lt_compat_l n m p : n < m -> p + n < p + m.
 Proof.
-  induction n; simpl; auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
-Hint Resolve le_plus_l: arith v62.
 
-Lemma le_plus_r : forall n m, m <= n + m.
+Lemma plus_lt_compat_r n m p : n < m -> n + p < m + p.
 Proof.
-  intros n m; elim n; simpl; auto with arith.
+ apply Nat.add_lt_mono_r.
 Qed.
-Hint Resolve le_plus_r: arith v62.
 
-Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p.
+Lemma plus_le_compat n m p q : n <= m -> p <= q -> n + p <= m + q.
 Proof.
-  intros; apply le_trans with (m := m); auto with arith.
+ apply Nat.add_le_mono.
 Qed.
-Hint Resolve le_plus_trans: arith v62.
 
-Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
+Lemma plus_le_lt_compat n m p q : n <= m -> p < q -> n + p < m + q.
 Proof.
-  intros; apply lt_le_trans with (m := m); auto with arith.
+ apply Nat.add_le_lt_mono.
 Qed.
-Hint Immediate lt_plus_trans: arith v62.
 
-Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
+Lemma plus_lt_le_compat n m p q : n < m -> p <= q -> n + p < m + q.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_lt_le_mono.
 Qed.
-Hint Resolve plus_lt_compat_l: arith v62.
 
-Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
+Lemma plus_lt_compat n m p q : n < m -> p < q -> n + p < m + q.
 Proof.
-  intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p).
-  elim p; auto with arith.
+ apply Nat.add_lt_mono.
 Qed.
-Hint Resolve plus_lt_compat_r: arith v62.
 
-Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
+Lemma le_plus_l n m : n <= n + m.
 Proof.
-  intros n m p q H H0.
-  elim H; simpl; auto with arith.
+ apply Nat.le_add_r.
 Qed.
 
-Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
+Lemma le_plus_r n m : m <= n + m.
 Proof.
-  unfold lt. intros. change (S n + p <= m + q). rewrite plus_Snm_nSm.
-  apply plus_le_compat; assumption.
+ rewrite Nat.add_comm. apply Nat.le_add_r.
 Qed.
 
-Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
+Theorem le_plus_trans n m p : n <= m -> n <= m + p.
 Proof.
-  unfold lt. intros. change (S n + p <= m + q). apply plus_le_compat; assumption.
+  intros. now rewrite <- Nat.le_add_r.
 Qed.
 
-Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Theorem lt_plus_trans n m p : n < m -> n < m + p.
 Proof.
-  intros. apply plus_lt_le_compat. assumption.
-  apply lt_le_weak. assumption.
+  intros. apply Nat.lt_le_trans with m. trivial. apply Nat.le_add_r.
 Qed.
 
 (** * Inversion lemmas *)
 
-Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0.
+Lemma plus_is_O n m : n + m = 0 -> n = 0 /\ m = 0.
 Proof.
-  intro m; destruct m as [| n]; auto.
-  intros. discriminate H.
+  destruct n; now split.
 Qed.
 
-Definition plus_is_one :
-  forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
+Definition plus_is_one m n :
+  m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
 Proof.
-  intro m; destruct m as [| n]; auto.
-  destruct n; auto.
-  intros.
-  simpl in H. discriminate H.
+  destruct m as [| m]; auto.
+  destruct m; auto.
+  discriminate.
 Defined.
 
 (** * Derived properties *)
 
-Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).
-Proof.
-  intros m n p q.
-  rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q).
-  rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc.
-Qed.
+Notation plus_permute_2_in_4 := Nat.add_shuffle1 (compat "8.4").
 
 (** * Tail-recursive plus *)
 
@@ -190,31 +153,37 @@ Fixpoint tail_plus n m : nat :=
   end.
 
 Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
+Proof.
 induction n as [| n IHn]; simpl; auto.
 intro m; rewrite <- IHn; simpl; auto.
 Qed.
 
 (** * Discrimination *)
 
-Lemma succ_plus_discr : forall n m, n <> S (plus m n).
+Lemma succ_plus_discr n m : n <> S (m+n).
 Proof.
-  intros n m; induction n as [|n IHn].
-  discriminate.
-  intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm;
-    reflexivity.
+ apply Nat.succ_add_discr.
 Qed.
 
-Lemma n_SSn : forall n, n <> S (S n).
-Proof.
-  intro n; exact (succ_plus_discr n 1).
-Qed.
+Lemma n_SSn n : n <> S (S n).
+Proof (succ_plus_discr n 1).
 
-Lemma n_SSSn : forall n, n <> S (S (S n)).
-Proof.
-  intro n; exact (succ_plus_discr n 2).
-Qed.
+Lemma n_SSSn n : n <> S (S (S n)).
+Proof (succ_plus_discr n 2).
 
-Lemma n_SSSSn : forall n, n <> S (S (S (S n))).
-Proof.
-  intro n; exact (succ_plus_discr n 3).
-Qed.
+Lemma n_SSSSn n : n <> S (S (S (S n))).
+Proof (succ_plus_discr n 3).
+
+
+(** * Compatibility Hints *)
+
+Hint Immediate plus_comm : arith v62.
+Hint Resolve plus_assoc plus_assoc_reverse : arith v62.
+Hint Resolve plus_le_compat_l plus_le_compat_r : arith v62.
+Hint Resolve le_plus_l le_plus_r le_plus_trans : arith v62.
+Hint Immediate lt_plus_trans : arith v62.
+Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith v62.
+
+(** For compatibility, we "Require" the same files as before *)
+
+Require Import Le Lt.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 05be5e1a3..2cb7c3c09 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -8,7 +8,7 @@
 
 (** Well-founded relations and natural numbers *)
 
-Require Import Lt.
+Require Import PeanoNat Lt.
 
 Local Open Scope nat_scope.
 
@@ -24,16 +24,12 @@ Definition gtof (a b:A) := f b > f a.
 
 Theorem well_founded_ltof : well_founded ltof.
 Proof.
-  red.
-  cut (forall n (a:A), f a < n -> Acc ltof a).
-  intros H a; apply (H (S (f a))); auto with arith.
-  induction n.
-  intros; absurd (f a < 0); auto with arith.
-  intros a ltSma.
-  apply Acc_intro.
-  unfold ltof; intros b ltfafb.
-  apply IHn.
-  apply lt_le_trans with (f a); auto with arith.
+  assert (H : forall n (a:A), f a < n -> Acc ltof a).
+  { induction n.
+    - intros; absurd (f a < 0); auto with arith.
+    - intros a Ha. apply Acc_intro. unfold ltof at 1. intros b Hb.
+      apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. }
+  intros a. apply (H (S (f a))). auto with arith.
 Defined.
 
 Theorem well_founded_gtof : well_founded gtof.
@@ -67,15 +63,13 @@ Theorem induction_ltof1 :
   forall P:A -> Set,
     (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
-  intros P F; cut (forall n (a:A), f a < n -> P a).
-  intros H a; apply (H (S (f a))); auto with arith.
-  induction n.
-  intros; absurd (f a < 0); auto with arith.
-  intros a ltSma.
-  apply F.
-  unfold ltof; intros b ltfafb.
-  apply IHn.
-  apply lt_le_trans with (f a); auto with arith.
+  intros P F.
+  assert (H : forall n (a:A), f a < n -> P a).
+  { induction n.
+    - intros; absurd (f a < 0); auto with arith.
+    - intros a Ha. apply F. unfold ltof. intros b Hb.
+      apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. }
+  intros a. apply (H (S (f a))). auto with arith.
 Defined.
 
 Theorem induction_gtof1 :
@@ -108,16 +102,12 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
 
 Theorem well_founded_lt_compat : well_founded R.
 Proof.
-  red.
-  cut (forall n (a:A), f a < n -> Acc R a).
-  intros H a; apply (H (S (f a))); auto with arith.
-  induction n.
-  intros; absurd (f a < 0); auto with arith.
-  intros a ltSma.
-  apply Acc_intro.
-  intros b ltfafb.
-  apply IHn.
-  apply lt_le_trans with (f a); auto with arith.
+  assert (H : forall n (a:A), f a < n -> Acc R a).
+  { induction n.
+    - intros; absurd (f a < 0); auto with arith.
+    - intros a Ha. apply Acc_intro. intros b Hb.
+      apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. }
+  intros a. apply (H (S (f a))). auto with arith.
 Defined.
 
 End Well_founded_Nat.
@@ -208,6 +198,7 @@ End LT_WF_REL.
 
 Lemma well_founded_inv_rel_inv_lt_rel :
   forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
+Proof.
   intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
 Qed.
 
@@ -230,30 +221,18 @@ Proof.
   intros P Pdec (n0,HPn0).
   assert
     (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
-      \/(forall n', P n' -> n<=n')).
-  induction n.
-  right.
-  intros n' Hn'.
-  apply le_O_n.
-  destruct IHn.
-  left; destruct H as (n', (Hlt', HPn')).
-  exists n'; split.
-  apply lt_S; assumption.
-  assumption.
-  destruct (Pdec n).
-  left; exists n; split.
-  apply lt_n_Sn.
-  split; assumption.
-  right.
-  intros n' Hltn'.
-  destruct (le_lt_eq_dec n n') as [Hltn|Heqn].
-  apply H; assumption.
-  assumption.
-  destruct H0.
-  rewrite Heqn; assumption.
-  destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
-    repeat split;
-      assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
+               \/ (forall n', P n' -> n<=n')).
+  { induction n.
+    - right. intros. apply Nat.le_0_l.
+    - destruct IHn as [(n' & IH1 & IH2)|IH].
+      + left. exists n'; auto with arith.
+      + destruct (Pdec n) as [HP|HP].
+        * left. exists n; auto with arith.
+        * right. intros n' Hn'.
+          apply Nat.le_neq; split; auto. intros <-. auto. }
+  destruct (H n0) as [(n & H1 & H2 & H3)|H0]; [exists n | exists n0];
+   repeat split; trivial;
+   intros n' (HPn',Hn'); apply Nat.le_antisymm; auto.
 Qed.
 
 Unset Implicit Arguments.
diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget
index 0b6564e15..0b3d31e98 100644
--- a/theories/Arith/vo.itarget
+++ b/theories/Arith/vo.itarget
@@ -1,3 +1,4 @@
+PeanoNat.vo
 Arith_base.vo
 Arith.vo
 Between.vo