24 files changed, 562 insertions, 375 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index be065f1d..18dbd27f 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Arith.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id$ i*)
 
 Require Export Arith_base.
 Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index fbdf2a41..2d54f0e8 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Arith_base.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Export Le.
 Require Export Lt.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 2e9472c4..208c2578 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Between.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Import Le.
 Require Import Lt.
@@ -17,11 +17,11 @@ Implicit Types k l p q r : nat.
 
 Section Between.
   Variables P Q : nat -> Prop.
-  
+
   Inductive between k : nat -> Prop :=
     | bet_emp : between k k
     | bet_S : forall l, between k l -> P l -> between k (S l).
-  
+
   Hint Constructors between: arith v62.
 
   Lemma bet_eq : forall k l, l = k -> between k l.
@@ -185,5 +185,5 @@ Section Between.
 End Between.
 
 Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
-  in_int_S in_int_intro: arith v62. 
+  in_int_S in_int_intro: arith v62.
 Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index fed650ab..9fd59e10 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Bool_nat.v 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id$ *)
 
 Require Export Compare_dec.
 Require Export Peano_dec.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 06898658..0f2595b2 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id$ i*)
 
 (** Equality is decidable on [nat] *)
 
@@ -52,4 +52,4 @@ Qed.
 
 Require Export Wf_nat.
 
-Require Export Min.
+Require Export Min Max.
\ No newline at end of file
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index e6cb5be4..8fc92579 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare_dec.v 10295 2007-11-06 22:46:21Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Import Le.
 Require Import Lt.
@@ -18,20 +18,24 @@ Open Local Scope nat_scope.
 Implicit Types m n x y : nat.
 
 Definition zerop n : {n = 0} + {0 < n}.
+Proof.
   destruct n; auto with arith.
 Defined.
 
-Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
-  induction n; simple destruct m; auto with arith.
-  intros m0; elim (IHn m0); auto with arith.
-  induction 1; auto with arith.
+Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}.
+Proof.
+  induction n; destruct m; auto with arith.
+  destruct (IHn m) as [H|H]; auto with arith.
+  destruct H; auto with arith.
 Defined.
 
-Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
-  exact lt_eq_lt_dec.
+Definition gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}.
+Proof.
+  intros; apply lt_eq_lt_dec; assumption.
 Defined.
 
-Definition le_lt_dec n m : {n <= m} + {m < n}.
+Definition le_lt_dec : forall n m, {n <= m} + {m < n}.
+Proof.
   induction n.
   auto with arith.
   destruct m.
@@ -40,43 +44,68 @@ Definition le_lt_dec n m : {n <= m} + {m < n}.
 Defined.
 
 Definition le_le_S_dec n m : {n <= m} + {S m <= n}.
-  exact le_lt_dec.
+Proof.
+  intros; 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.
 Defined.
 
 Definition le_gt_dec n m : {n <= m} + {n > m}.
-  exact le_lt_dec.
+Proof.
+  intros; exact (le_lt_dec n m).
 Defined.
 
 Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
-  intros; elim (lt_eq_lt_dec n m); auto with arith.
+Proof.
+  intros; destruct (lt_eq_lt_dec n m); auto with arith.
   intros; absurd (m < n); auto with arith.
 Defined.
 
+Theorem le_dec : forall 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.
+Defined.
+
+Theorem lt_dec : forall n m, {n < m} + {~ n < m}.
+Proof.
+  intros; apply le_dec.
+Defined.
+
+Theorem gt_dec : forall n m, {n > m} + {~ n > m}.
+Proof.
+  intros; apply lt_dec.
+Defined.
+
+Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}.
+Proof.
+  intros; apply le_dec.
+Defined.
+
 (** Proofs of decidability *)
 
 Theorem dec_le : forall n m, decidable (n <= m).
 Proof.
-  intros x y; unfold decidable in |- *; elim (le_gt_dec x y);
-    [ auto with arith | intro; right; apply gt_not_le; assumption ].
+  intros n m; destruct (le_dec n m); unfold decidable; auto.
 Qed.
 
 Theorem dec_lt : forall n m, decidable (n < m).
 Proof.
-  intros x y; unfold lt in |- *; apply dec_le.
+  intros; apply dec_le.
 Qed.
 
 Theorem dec_gt : forall n m, decidable (n > m).
 Proof.
-  intros x y; unfold gt in |- *; apply dec_lt.
+  intros; apply dec_lt.
 Qed.
 
 Theorem dec_ge : forall n m, decidable (n >= m).
 Proof.
-  intros x y; unfold ge in |- *; apply dec_le.
+  intros; apply dec_le.
 Qed.
 
 Theorem not_eq : forall n m, n <> m -> n < m \/ m < n.
@@ -107,86 +136,111 @@ Qed.
 
 Theorem not_lt : forall n m, ~ n < m -> n >= m.
 Proof.
-  intros x y H; exact (not_gt y x H). 
+  intros x y H; exact (not_gt y x H).
 Qed.
 
 
 (** A ternary comparison function in the spirit of [Zcompare]. *)
 
-Definition nat_compare (n m:nat) :=
-  match lt_eq_lt_dec n m with 
-    | inleft (left _) => Lt
-    | inleft (right _) => Eq
-    | inright _ => Gt
+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.
 
 Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m.
 Proof.
-  unfold nat_compare; intros.
-  simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto.
+ reflexivity.
+Qed.
+
+Lemma nat_compare_eq_iff : forall n m, nat_compare n m = Eq <-> n = m.
+Proof.
+  induction n; destruct m; simpl; split; auto; try discriminate;
+   destruct (IHn m); auto.
 Qed.
 
 Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m.
 Proof.
-  induction n; destruct m; simpl; auto.
-  unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  rewrite nat_compare_S; auto.
+  intros; apply -> nat_compare_eq_iff; auto.
 Qed.
 
 Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt.
 Proof.
-  induction n; destruct m; simpl.
-  unfold nat_compare; simpl; intuition; [inversion H | discriminate H].
-  split; auto with arith.
-  split; [inversion 1 |].
-  unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  rewrite nat_compare_S.
-  generalize (IHn m); clear IHn; intuition.
+  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.
 Qed.
 
 Lemma nat_compare_gt : forall n m, n>m <-> nat_compare n m = Gt.
 Proof.
-  induction n; destruct m; simpl.
-  unfold nat_compare; simpl; intuition; [inversion H | discriminate H].
-  split; [inversion 1 |].
-  unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  split; auto with arith.
-  rewrite nat_compare_S.
-  generalize (IHn m); clear IHn; intuition.
+  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.
 Qed.
 
 Lemma nat_compare_le : forall n m, n<=m <-> nat_compare n m <> Gt.
 Proof.
   split.
-  intros.
-  intro.
-  destruct (nat_compare_gt n m).
-  generalize (le_lt_trans _ _ _ H (H2 H0)).
-  exact (lt_irrefl n).
-  intros.
-  apply not_gt.
-  contradict H.
-  destruct (nat_compare_gt n m); auto.
-Qed.  
+  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.
-  intro.
-  destruct (nat_compare_lt n m).
-  generalize (le_lt_trans _ _ _ H (H2 H0)).
-  exact (lt_irrefl m).
-  intros.
-  apply not_lt.
-  contradict H.
-  destruct (nat_compare_lt n m); auto.
-Qed.  
+  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.
+
+Lemma nat_compare_spec : forall x y, CompSpec eq lt x y (nat_compare x y).
+Proof.
+ intros.
+ destruct (nat_compare x y) as [ ]_eqn; constructor.
+ apply nat_compare_eq; auto.
+ apply <- nat_compare_lt; auto.
+ apply <- nat_compare_gt; auto.
+Qed.
+
+
+(** Some projections of the above equivalences. *)
+
+Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m.
+Proof.
+  intros; apply <- nat_compare_lt; auto.
+Qed.
+
+Lemma nat_compare_Gt_gt : forall n m, nat_compare n m = Gt -> n>m.
+Proof.
+  intros; apply <- nat_compare_gt; auto.
+Qed.
+
+(** A previous definition of [nat_compare] in terms of [lt_eq_lt_dec].
+    The new version avoids the creation of proof parts. *)
+
+Definition nat_compare_alt (n m:nat) :=
+  match lt_eq_lt_dec n m with
+    | inleft (left _) => Lt
+    | inleft (right _) => Eq
+    | inright _ => Gt
+  end.
+
+Lemma nat_compare_equiv: forall n m,
+ nat_compare 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.
+Qed.
+
 
 (** A boolean version of [le] over [nat]. *)
 
@@ -200,48 +254,48 @@ Fixpoint leb (m:nat) : nat -> bool :=
                    end
   end.
 
-Lemma leb_correct : forall m n:nat, m <= n -> leb m n = true.
+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 in |- *. apply IHm. apply le_S_n. assumption.
 Qed.
 
-Lemma leb_complete : forall m n:nat, leb m n = true -> m <= n.
+Lemma leb_complete : forall m n, leb m n = true -> m <= n.
 Proof.
   induction m. trivial with arith.
   destruct n. intro H. discriminate H.
   auto with arith.
 Qed.
 
-Lemma leb_correct_conv : forall m n:nat, m < n -> leb n m = false.
+Lemma leb_iff : forall m n, leb m n = true <-> m <= n.
 Proof.
-  intros. 
+  split; auto using leb_correct, leb_complete.
+Qed.
+
+Lemma leb_correct_conv : forall m n, m < n -> leb n m = false.
+Proof.
+  intros.
   generalize (leb_complete n m).
   destruct (leb n m); auto.
-  intros.
-  elim (lt_irrefl _ (lt_le_trans _ _ _ H (H0 (refl_equal true)))).
+  intros; elim (lt_not_le m n); auto.
 Qed.
 
-Lemma leb_complete_conv : forall m n:nat, leb n m = false -> m < n.
+Lemma leb_complete_conv : forall m n, leb n m = false -> m < n.
 Proof.
-  intros. elim (le_or_lt n m). intro. conditional trivial rewrite leb_correct in H. discriminate H.
-  trivial.
+  intros m n EQ. apply not_le.
+  intro LE. apply leb_correct in LE. rewrite LE in EQ; discriminate.
+Qed.
+
+Lemma leb_iff_conv : forall m n, leb n m = false <-> m < n.
+Proof.
+  split; auto using leb_complete_conv, leb_correct_conv.
 Qed.
 
 Lemma leb_compare : forall n m, leb n m = true <-> nat_compare n m <> Gt.
 Proof.
- induction n; destruct m; simpl.
- unfold nat_compare; simpl.
- intuition; discriminate.
- split; auto with arith.
- unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H]; 
-  intuition; try discriminate.
- inversion H.
- split; try (intros; discriminate).
- unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H]; 
-  intuition; try discriminate.
- inversion H.
- rewrite nat_compare_S; auto.
-Qed. 
+ split; intros.
+ apply -> nat_compare_le. auto using leb_complete.
+ apply leb_correct. apply <- nat_compare_le; auto.
+Qed.
 
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 7cab976f..999a6454 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Div2.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Import Lt.
 Require Import Plus.
@@ -36,7 +36,7 @@ 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.
 Qed.
@@ -150,7 +150,7 @@ Proof fun n => proj2 (proj2 (even_odd_double n)).
 
 Hint Resolve even_double double_even odd_double double_odd: arith.
 
-(** Application: 
+(** Application:
     - if [n] is even then there is a [p] such that [n = 2p]
     - if [n] is odd  then there is a [p] such that [n = 2p+1]
 
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index a9244455..312b76e9 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqNat.v 9966 2007-07-10 23:54:53Z letouzey $ i*)
+(*i $Id$ i*)
 
 (** Equality on natural numbers *)
 
@@ -16,7 +16,7 @@ Implicit Types m n x y : nat.
 
 (** * Propositional equality  *)
 
-Fixpoint eq_nat n m {struct n} : Prop :=
+Fixpoint eq_nat n m : Prop :=
   match n, m with
     | O, O => True
     | O, S _ => False
@@ -68,7 +68,7 @@ Defined.
 
 (** * Boolean equality on [nat] *)
 
-Fixpoint beq_nat n m {struct n} : bool :=
+Fixpoint beq_nat n m : bool :=
   match n, m with
     | O, O => true
     | O, S _ => false
@@ -99,3 +99,18 @@ Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
 Proof.
  induction x; destruct y; simpl; auto; intros; discriminate.
 Qed.
+
+Lemma beq_nat_true_iff : forall x y, beq_nat x y = true <-> x=y.
+Proof.
+ split. apply beq_nat_true.
+ intros; subst; symmetry; apply beq_nat_refl.
+Qed.
+
+Lemma beq_nat_false_iff : forall x y, beq_nat x y = false <-> x<>y.
+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.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 3d6f1af5..f50dcc84 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Euclid.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Import Mult.
 Require Import Compare_dec.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 59209370..eaa1bb2d 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Even.v 11512 2008-10-27 12:28:36Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
@@ -17,7 +17,7 @@ Open Local Scope nat_scope.
 Implicit Types m n : nat.
 
 
-(** * Definition of [even] and [odd], and basic facts *) 
+(** * Definition of [even] and [odd], and basic facts *)
 
 Inductive even : nat -> Prop :=
   | even_O : even 0
@@ -52,9 +52,9 @@ Qed.
 
 (** * Facts about [even] & [odd] wrt. [plus] *)
 
-Lemma even_plus_split : forall n m, 
+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, 
+with odd_plus_split : forall n m,
   odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
 Proof.
 intros. clear even_plus_split. destruct n; simpl in *.
@@ -95,7 +95,7 @@ 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_l : forall n m, even (n + m) -> even m -> even n.
 Proof.
   intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
@@ -120,13 +120,13 @@ 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_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_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.
@@ -203,7 +203,7 @@ Proof.
   intros n m; case (even_mult_aux n m); auto.
   intros H H0; case H0; auto.
 Qed.
- 
+
 Lemma even_mult_r : forall n m, even m -> even (n * m).
 Proof.
   intros n m; case (even_mult_aux n m); auto.
@@ -219,7 +219,7 @@ Proof.
   intros H'3; elim H'3; auto.
   intros H; case (not_even_and_odd n); auto.
 Qed.
- 
+
 Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.
 Proof.
   intros n m H' H'0.
@@ -228,13 +228,13 @@ Proof.
   intros H'3; elim H'3; auto.
   intros H; case (not_even_and_odd m); auto.
 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_inv_l : forall n m, odd (n * m) -> odd n.
 Proof.
   intros n m H'.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 5e2f491a..8c531562 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Factorial.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Import Plus.
 Require Import Mult.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 5b1ee1b2..70169f52 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Gt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 (** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
 <<
@@ -135,7 +135,7 @@ Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
 
 (** * Comparison to 0 *)
 
-Theorem gt_O_eq : forall n, n > 0 \/ 0 = n.
+Theorem gt_0_eq : forall n, n > 0 \/ 0 = n.
 Proof.
   intro n; apply gt_S; auto with arith.
 Qed.
@@ -151,4 +151,8 @@ Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
 Proof.
   auto with arith.
 Qed.
-Hint Resolve plus_gt_compat_l: arith v62.
\ No newline at end of file
+Hint Resolve plus_gt_compat_l: arith v62.
+
+(* begin hide *)
+Notation gt_O_eq := gt_0_eq (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index e8b9e6be..d85178de 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Le.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 (** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
 <<
@@ -41,25 +41,25 @@ Hint Resolve le_trans: arith v62.
 
 (** Comparison to 0 *)
 
-Theorem le_O_n : forall n, 0 <= n.
+Theorem le_0_n : forall n, 0 <= n.
 Proof.
   induction n; auto.
 Qed.
 
-Theorem le_Sn_O : forall n, ~ S n <= 0.
+Theorem le_Sn_0 : forall n, ~ S n <= 0.
 Proof.
   red in |- *; intros n H.
   change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
 Qed.
 
-Hint Resolve le_O_n le_Sn_O: arith v62.
+Hint Resolve le_0_n le_Sn_0: arith v62.
 
-Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n.
+Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n.
 Proof.
   induction n; auto with arith.
-  intro; contradiction le_Sn_O with n.
+  intro; contradiction le_Sn_0 with n.
 Qed.
-Hint Immediate le_n_O_eq: arith v62.
+Hint Immediate le_n_0_eq: arith v62.
 
 
 (** [le] and successor *)
@@ -135,3 +135,9 @@ Proof.
   intros m Le.
   elim Le; auto with arith.
 Qed.
+
+(* begin hide *)
+Notation le_O_n := le_0_n (only parsing).
+Notation le_Sn_O := le_Sn_0 (only parsing).
+Notation le_n_O_eq := le_n_0_eq (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 94cf3793..af435e54 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Lt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 (** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
 <<
@@ -26,7 +26,7 @@ Theorem lt_irrefl : forall n, ~ n < n.
 Proof le_Sn_n.
 Hint Resolve lt_irrefl: arith v62.
 
-(** * Relationship between [le] and [lt] *) 
+(** * Relationship between [le] and [lt] *)
 
 Theorem lt_le_S : forall n m, n < m -> S n <= m.
 Proof.
@@ -90,11 +90,11 @@ Proof.
 Qed.
 Hint Immediate lt_S_n: arith v62.
 
-Theorem lt_O_Sn : forall n, 0 < S n.
+Theorem lt_0_Sn : forall n, 0 < S n.
 Proof.
   auto with arith.
 Qed.
-Hint Resolve lt_O_Sn: arith v62.
+Hint Resolve lt_0_Sn: arith v62.
 
 Theorem lt_n_O : forall n, ~ n < 0.
 Proof le_Sn_O.
@@ -144,6 +144,13 @@ Proof.
   induction 1; auto with arith.
 Qed.
 
+Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Proof.
+  split.
+  intros; apply le_lt_or_eq; auto.
+  destruct 1; subst; auto with arith.
+Qed.
+
 Theorem lt_le_weak : forall n m, n < m -> n <= m.
 Proof.
   auto with arith.
@@ -168,15 +175,21 @@ Qed.
 
 (** * Comparison to 0 *)
 
-Theorem neq_O_lt : forall n, 0 <> n -> 0 < n.
+Theorem neq_0_lt : forall n, 0 <> n -> 0 < n.
 Proof.
   induction n; auto with arith.
   intros; absurd (0 = 0); trivial with arith.
 Qed.
-Hint Immediate neq_O_lt: arith v62.
+Hint Immediate neq_0_lt: arith v62.
 
-Theorem lt_O_neq : forall n, 0 < n -> 0 <> n.
+Theorem lt_0_neq : forall n, 0 < n -> 0 <> n.
 Proof.
   induction 1; auto with arith.
 Qed.
-Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file
+Hint Immediate lt_0_neq: arith v62.
+
+(* begin hide *)
+Notation lt_O_Sn := lt_0_Sn (only parsing).
+Notation neq_O_lt := neq_0_lt (only parsing).
+Notation lt_O_neq := lt_0_neq (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 5de2298d..3d7fe9fc 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,81 +6,39 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
-
-Require Import Le.
-
-Open Local Scope nat_scope.
-
-Implicit Types m n : nat.
-
-(** * maximum of two natural numbers *)
-
-Fixpoint max n m {struct n} : nat :=
-  match n, m with
-    | O, _ => m
-    | S n', O => n
-    | S n', S m' => S (max n' m')
-  end.
-
-(** * Simplifications of [max] *)
-
-Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
-Proof.
-  auto with arith.
-Qed.
-
-Theorem max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
-Proof.
-  induction m; destruct n; destruct p; trivial.
-  simpl.
-  auto using IHm.
-Qed.
-
-Lemma max_comm : forall n m, max n m = max m n.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-(** * [max] and [le] *)
-
-Lemma max_l : forall n m, m <= n -> max n m = n.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma max_r : forall n m, n <= m -> max n m = m.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_max_l : forall n m, n <= max n m.
-Proof.
-  induction n; intros; simpl in |- *; auto with arith.
-  elim m; intros; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_max_r : forall n m, m <= max n m.
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; simpl in |- *; auto with arith.
-Qed.
-Hint Resolve max_r max_l le_max_l le_max_r: arith v62.
-
-
-(** * [max n m] is equal to [n] or [m] *)
-
-Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-  elim (IHn m); intro H; elim H; auto.
-Defined.
-
-Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; intros; simpl in |- *; auto with arith.
-  pattern (max n m) in |- *; apply IHn; auto with arith.
-Defined.
-
+(*i $Id$ i*)
+
+(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
+
+Require Export MinMax.
+
+Local Open Scope nat_scope.
+Implicit Types m n p : nat.
+
+Notation max := MinMax.max (only parsing).
+
+Definition max_0_l := max_0_l.
+Definition max_0_r := max_0_r.
+Definition succ_max_distr := succ_max_distr.
+Definition plus_max_distr_l := plus_max_distr_l.
+Definition plus_max_distr_r := plus_max_distr_r.
+Definition max_case_strong := max_case_strong.
+Definition max_spec := max_spec.
+Definition max_dec := max_dec.
+Definition max_case := max_case.
+Definition max_idempotent := max_id.
+Definition max_assoc := max_assoc.
+Definition max_comm := max_comm.
+Definition max_l := max_l.
+Definition max_r := max_r.
+Definition le_max_l := le_max_l.
+Definition le_max_r := le_max_r.
+Definition max_lub_l := max_lub_l.
+Definition max_lub_r := max_lub_r.
+Definition max_lub := max_lub.
+
+(* begin hide *)
+(* Compatibility *)
 Notation max_case2 := max_case (only parsing).
+Notation max_SS := succ_max_distr (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index aa009963..c52fc0dd 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -6,91 +6,39 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Min.v 9660 2007-02-19 11:36:30Z notin $ i*)
+(*i $Id$ i*)
 
-Require Import Le.
+(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
 
-Open Local Scope nat_scope.
-
-Implicit Types m n : nat.
-
-(** * minimum of two natural numbers *)
-
-Fixpoint min n m {struct n} : nat :=
-  match n, m with
-    | O, _ => 0
-    | S n', O => 0
-    | S n', S m' => S (min n' m')
-  end.
-
-(** * Simplifications of [min] *)
-
-Lemma min_0_l : forall n : nat, min 0 n = 0.
-Proof.
-  trivial. 
-Qed.
-
-Lemma min_0_r : forall n : nat, min n 0 = 0.
-Proof.
-  destruct n; trivial.
-Qed.
-
-Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
-Proof.
-  auto with arith.
-Qed.
-
-Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p.
-Proof.
-  induction m; destruct n; destruct p; trivial.
-  simpl.
-  auto using (IHm n p).
-Qed.
-
-Lemma min_comm : forall n m, min n m = min m n.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-(** * [min] and [le] *)
-
-Lemma min_l : forall n m, n <= m -> min n m = n.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma min_r : forall n m, m <= n -> min n m = m.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_min_l : forall n m, min n m <= n.
-Proof.
-  induction n; intros; simpl in |- *; auto with arith.
-  elim m; intros; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_min_r : forall n m, min n m <= m.
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; simpl in |- *; auto with arith.
-Qed.
-Hint Resolve min_l min_r le_min_l le_min_r: arith v62.
-
-(** * [min n m] is equal to [n] or [m] *)
-
-Lemma min_dec : forall n m, {min n m = n} + {min n m = m}.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-  elim (IHn m); intro H; elim H; auto.
-Qed.
-
-Lemma min_case : forall n m (P:nat -> Type), P n -> P m -> P (min n m).
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; intros; simpl in |- *; auto with arith.
-  pattern (min n m) in |- *; apply IHn; auto with arith.
-Qed.
+Require Export MinMax.
 
+Open Local Scope nat_scope.
+Implicit Types m n p : nat.
+
+Notation min := MinMax.min (only parsing).
+
+Definition min_0_l := min_0_l.
+Definition min_0_r := min_0_r.
+Definition succ_min_distr := succ_min_distr.
+Definition plus_min_distr_l := plus_min_distr_l.
+Definition plus_min_distr_r := plus_min_distr_r.
+Definition min_case_strong := min_case_strong.
+Definition min_spec := min_spec.
+Definition min_dec := min_dec.
+Definition min_case := min_case.
+Definition min_idempotent := min_id.
+Definition min_assoc := min_assoc.
+Definition min_comm := min_comm.
+Definition min_l := min_l.
+Definition min_r := min_r.
+Definition le_min_l := le_min_l.
+Definition le_min_r := le_min_r.
+Definition min_glb_l := min_glb_l.
+Definition min_glb_r := min_glb_r.
+Definition min_glb := min_glb.
+
+(* begin hide *)
+(* Compatibility *)
 Notation min_case2 := min_case (only parsing).
-
+Notation min_SS := succ_min_distr (only parsing).
+(* end hide *)
\ No newline at end of file
diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v
new file mode 100644
index 00000000..6e86a88c
--- /dev/null
+++ b/theories/Arith/MinMax.v
@@ -0,0 +1,113 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Orders NatOrderedType GenericMinMax.
+
+(** * Maximum and Minimum of two natural numbers *)
+
+Fixpoint max n m : nat :=
+  match n, m with
+    | O, _ => m
+    | S n', O => n
+    | S n', S m' => S (max n' m')
+  end.
+
+Fixpoint min n m : nat :=
+  match n, m with
+    | O, _ => 0
+    | S n', O => 0
+    | S n', S m' => S (min n' m')
+  end.
+
+(** These functions implement indeed a maximum and a minimum *)
+
+Lemma max_l : forall x y, y<=x -> max x y = x.
+Proof.
+ induction x; destruct y; simpl; auto with arith.
+Qed.
+
+Lemma max_r : forall x y, x<=y -> max x y = y.
+Proof.
+ induction x; destruct y; simpl; auto with arith.
+Qed.
+
+Lemma min_l : forall x y, x<=y -> min x y = x.
+Proof.
+ induction x; destruct y; simpl; auto with arith.
+Qed.
+
+Lemma min_r : forall x y, y<=x -> min x y = y.
+Proof.
+ induction x; destruct y; simpl; auto with arith.
+Qed.
+
+
+Module NatHasMinMax <: HasMinMax Nat_as_OT.
+ Definition max := max.
+ Definition min := min.
+ Definition max_l := max_l.
+ Definition max_r := max_r.
+ Definition min_l := min_l.
+ Definition min_r := min_r.
+End NatHasMinMax.
+
+(** We obtain hence all the generic properties of [max] and [min],
+    see file [GenericMinMax] or use SearchAbout. *)
+
+Module Export MMP := UsualMinMaxProperties Nat_as_OT NatHasMinMax.
+
+
+(** * Properties specific to the [nat] domain *)
+
+(** Simplifications *)
+
+Lemma max_0_l : forall n, max 0 n = n.
+Proof. reflexivity. Qed.
+
+Lemma max_0_r : forall n, max n 0 = n.
+Proof. destruct n; auto. Qed.
+
+Lemma min_0_l : forall n, min 0 n = 0.
+Proof. reflexivity. Qed.
+
+Lemma min_0_r : forall n, min n 0 = 0.
+Proof. destruct n; auto. Qed.
+
+(** Compatibilities (consequences of monotonicity) *)
+
+Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m).
+Proof. auto. Qed.
+
+Lemma succ_min_distr : forall n m, S (min n m) = min (S n) (S m).
+Proof. auto. Qed.
+
+Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m.
+Proof.
+intros. apply max_monotone. repeat red; auto with arith.
+Qed.
+
+Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p.
+Proof.
+intros. apply max_monotone with (f:=fun x => x + p).
+repeat red; auto with arith.
+Qed.
+
+Lemma plus_min_distr_l : forall n m p, min (p + n) (p + m) = p + min n m.
+Proof.
+intros. apply min_monotone. repeat red; auto with arith.
+Qed.
+
+Lemma plus_min_distr_r : forall n m p, min (n + p) (m + p) = min n m + p.
+Proof.
+intros. apply min_monotone with (f:=fun x => x + p).
+repeat red; auto with arith.
+Qed.
+
+Hint Resolve
+ max_l max_r le_max_l le_max_r
+ min_l min_r le_min_l le_min_r : arith v62.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index b961886d..cd6c0a29 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Minus.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
 <<
-Fixpoint minus (n m:nat) {struct n} : nat :=
+Fixpoint minus (n m:nat) : nat :=
   match n, m with
   | O, _ => n
   | S k, O => S k
@@ -120,10 +120,10 @@ Proof.
 
     intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
       intros q; destruct q; auto with arith.
-        simpl. 
+        simpl.
         apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
           auto with arith.
-        
+
       intros q r Hqr _. simpl. auto using HI.
 Qed.
 
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index a43579f9..8346cae3 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Mult.v 11015 2008-05-28 20:06:42Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Export Plus.
 Require Export Minus.
@@ -43,7 +43,7 @@ Hint Resolve mult_1_l: arith v62.
 
 Lemma mult_1_r : forall n, n * 1 = n.
 Proof.
-  induction n; [ trivial | 
+  induction n; [ trivial |
     simpl; rewrite IHn; reflexivity].
 Qed.
 Hint Resolve mult_1_r: arith v62.
@@ -52,9 +52,9 @@ Hint Resolve mult_1_r: arith v62.
 
 Lemma mult_comm : forall n m, n * m = m * n.
 Proof.
-intros; elim n; intros; simpl in |- *; auto with arith.
-elim mult_n_Sm.
-elim H; apply plus_comm.
+intros; induction n; simpl; auto with arith.
+rewrite <- mult_n_Sm.
+rewrite IHn; apply plus_comm.
 Qed.
 Hint Resolve mult_comm: arith v62.
 
@@ -62,29 +62,28 @@ Hint Resolve mult_comm: arith v62.
 
 Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
 Proof.
-  intros; elim n; simpl in |- *; intros; auto with arith.
-  elim plus_assoc; elim H; auto with arith.
+  intros; induction n; simpl; auto with arith.
+  rewrite <- plus_assoc, IHn; auto with arith.
 Qed.
 Hint Resolve mult_plus_distr_r: arith v62.
 
 Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
 Proof.
   induction n. trivial.
-  intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4.
+  intros. simpl in |- *. rewrite IHn. symmetry. apply plus_permute_2_in_4.
 Qed.
 
 Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
 Proof.
-  intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros;
-    auto with arith.
-  elim minus_plus_simpl_l_reverse; auto with arith.
+  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.
 
 Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p.
 Proof.
-  intros n m p. rewrite mult_comm. rewrite mult_minus_distr_r. 
-  rewrite (mult_comm m n); rewrite (mult_comm p n); reflexivity.
+  intros n m p.
+  rewrite mult_comm, mult_minus_distr_r, (mult_comm m n), (mult_comm p n); reflexivity.
 Qed.
 Hint Resolve mult_minus_distr_l: arith v62.
 
@@ -92,9 +91,9 @@ Hint Resolve mult_minus_distr_l: arith v62.
 
 Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
 Proof.
-  intros; elim n; intros; simpl in |- *; auto with arith.
+  intros; induction n; simpl; auto with arith.
   rewrite mult_plus_distr_r.
-  elim H; auto with arith.
+  induction IHn; auto with arith.
 Qed.
 Hint Resolve mult_assoc_reverse: arith v62.
 
@@ -108,23 +107,18 @@ Hint Resolve mult_assoc: arith v62.
 
 Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
 Proof.
-  destruct n as [| n]. 
-    intros; left; trivial.
-
-    simpl; intros m H; right. 
-    assert (H':m = 0 /\ n * m = 0) by apply (plus_is_O _ _ H).
-    destruct H'; trivial.
+  destruct n as [| n]; simpl; intros m H.
+    left; trivial.
+    right; apply plus_is_O in H; destruct H; trivial.
 Qed.
 
 Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
 Proof.
-  destruct n as [|n].
-    simpl; intros m H; elim (O_S _ H).
-
-    simpl; intros m H.
-    destruct (plus_is_one _ _ H) as [[Hm Hnm] | [Hm Hnm]].
-      rewrite Hm in H; simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
-      rewrite Hm in Hnm; rewrite mult_1_r in Hnm; auto. 
+  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.
 Qed.
 
 (** ** Multiplication and successor *)
@@ -151,18 +145,16 @@ Hint Resolve mult_O_le: arith v62.
 
 Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
 Proof.
-  induction p as [| p IHp]. intros. simpl in |- *. apply le_n.
-  intros. simpl in |- *. apply plus_le_compat. assumption.
-  apply IHp. assumption.
+  induction p as [| p IHp]; intros; simpl in |- *.
+  apply le_n.
+  auto using plus_le_compat.
 Qed.
 Hint Resolve mult_le_compat_l: arith.
 
 
 Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
 Proof.
-  intros m n p H.
-  rewrite mult_comm. rewrite (mult_comm n).
-  auto with arith.
+  intros m n p H; rewrite mult_comm, (mult_comm n); auto with arith.
 Qed.
 
 Lemma mult_le_compat :
@@ -184,8 +176,9 @@ Qed.
 
 Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
 Proof.
-  intro m; induction m. intros. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption.
-  intros. exact (plus_lt_compat _ _ _ _ H (IHm _ _ H)).
+  induction n; intros; simpl in *.
+    rewrite <- 2! plus_n_O; assumption.
+    auto using plus_lt_compat.
 Qed.
 
 Hint Resolve mult_S_lt_compat_l: arith.
@@ -201,40 +194,36 @@ Qed.
 
 Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
 Proof.
-  intros m n p H. elim (le_or_lt n p). trivial.
-  intro H0. cut (S m * n < S m * n). intro. elim (lt_irrefl _ H1).
-  apply le_lt_trans with (m := S m * p). assumption.
-  apply mult_S_lt_compat_l. assumption.
+  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).
 Qed.
 
 (** * n|->2*n and n|->2n+1 have disjoint image *)
 
 Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.
 Proof.
-  intros p; elim p; auto.
-  intros q; case q; simpl in |- *.
-  red in |- *; intros; discriminate.
-  intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *;
-    intros; discriminate.
-  intros p' H q; case q.
-  simpl in |- *; red in |- *; intros; discriminate.
-  intros q'; red in |- *; intros H0; case (H q').
-  replace (2 * q') with (2 * S q' - 2).
-  rewrite <- H0; simpl in |- *; auto.
-  repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto.
-  simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *;
-    auto.
-  case q'; simpl in |- *; auto.
+  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.
 Qed.
 
 
 (** * Tail-recursive mult *)
 
-(** [tail_mult] is an alternative definition for [mult] which is 
-    tail-recursive, whereas [mult] is not. This can be useful 
+(** [tail_mult] is an alternative definition for [mult] which is
+    tail-recursive, whereas [mult] is not. This can be useful
     when extracting programs. *)
 
-Fixpoint mult_acc (s:nat) m n {struct n} : nat :=
+Fixpoint mult_acc (s:nat) m n : nat :=
   match n with
     | O => s
     | S p => mult_acc (tail_plus m s) m p
@@ -244,7 +233,7 @@ Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 Proof.
   induction n as [| p IHp]; simpl in |- *; auto.
   intros s m; rewrite <- plus_tail_plus; rewrite <- IHp.
-  rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto.
+  rewrite <- plus_assoc_reverse; apply f_equal2; auto.
   rewrite plus_comm; auto.
 Qed.
 
@@ -255,7 +244,7 @@ Proof.
   intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
 Qed.
 
-(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] 
+(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus]
     and [mult] and simplify *)
 
 Ltac tail_simpl :=
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
new file mode 100644
index 00000000..df5b37e0
--- /dev/null
+++ b/theories/Arith/NatOrderedType.v
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Lt Peano_dec Compare_dec EqNat
+ Equalities Orders OrdersTac.
+
+
+(** * DecidableType structure for Peano numbers *)
+
+Module Nat_as_UBE <: UsualBoolEq.
+ Definition t := nat.
+ Definition eq := @eq nat.
+ Definition eqb := beq_nat.
+ Definition eqb_eq := beq_nat_true_iff.
+End Nat_as_UBE.
+
+Module Nat_as_DT <: UsualDecidableTypeFull := Make_UDTF Nat_as_UBE.
+
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
+
+
+
+(** * OrderedType structure for Peano numbers *)
+
+Module Nat_as_OT <: OrderedTypeFull.
+ Include Nat_as_DT.
+ Definition lt := lt.
+ Definition le := le.
+ Definition compare := nat_compare.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed.
+
+ Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt.
+ Proof. repeat red; intros; subst; auto. Qed.
+
+ Definition le_lteq := le_lt_or_eq_iff.
+ Definition compare_spec := nat_compare_spec.
+
+End Nat_as_OT.
+
+(** Note that [Nat_as_OT] can also be seen as a [UsualOrderedType]
+   and a [OrderedType] (and also as a [DecidableType]). *)
+
+
+
+(** * An [order] tactic for Peano numbers *)
+
+Module NatOrder := OTF_to_OrderTac Nat_as_OT.
+Ltac nat_order := NatOrder.order.
+
+(** 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 Test.
+Let test : forall x y : nat, x<=y -> y<=x -> x=y.
+Proof. nat_order. Qed.
+End Test.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index cc970ae4..42335f98 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Peano_dec.v 9698 2007-03-12 17:11:32Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Import Decidable.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 6d510447..9b7c6261 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Plus.v 9750 2007-04-06 00:58:14Z letouzey $ i*)
+(*i $Id$ i*)
 
 (** Properties of addition. [add] is defined in [Init/Peano.v] as:
 <<
-Fixpoint plus (n m:nat) {struct n} : nat :=
+Fixpoint plus (n m:nat) : nat :=
   match n with
   | O => m
   | S p => S (p + m)
@@ -65,7 +65,7 @@ Qed.
 Hint Resolve plus_assoc: arith v62.
 
 Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p).
-Proof. 
+Proof.
   intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith.
 Qed.
 
@@ -179,7 +179,7 @@ Definition plus_is_one :
 Proof.
   intro m; destruct m as [| n]; auto.
   destruct n; auto.
-  intros. 
+  intros.
   simpl in H. discriminate H.
 Defined.
 
@@ -187,18 +187,18 @@ Defined.
 
 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. 
+  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.
 
 (** * Tail-recursive plus *)
 
-(** [tail_plus] is an alternative definition for [plus] which is 
+(** [tail_plus] is an alternative definition for [plus] which is
     tail-recursive, whereas [plus] is not. This can be useful
     when extracting programs. *)
 
-Fixpoint tail_plus n m {struct n} : nat :=
+Fixpoint tail_plus n m : nat :=
   match n with
     | O => m
     | S n => tail_plus n (S m)
@@ -215,7 +215,7 @@ Lemma succ_plus_discr : forall n m, n <> S (plus 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; 
+  intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm;
     reflexivity.
 Qed.
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 6ad640eb..5bc5d2a5 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Wf_nat.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Well-founded relations and natural numbers *)
 
@@ -46,9 +46,9 @@ Defined.
 (** It is possible to directly prove the induction principle going
    back to primitive recursion on natural numbers ([induction_ltof1])
    or to use the previous lemmas to extract a program with a fixpoint
-   ([induction_ltof2]) 
+   ([induction_ltof2])
 
-the ML-like program for [induction_ltof1] is : 
+the ML-like program for [induction_ltof1] is :
 [[
 let induction_ltof1 f F a =
   let rec indrec n k =
@@ -58,7 +58,7 @@ let induction_ltof1 f F a =
   in indrec (f a + 1) a
 ]]
 
-the ML-like program for [induction_ltof2] is : 
+the ML-like program for [induction_ltof2] is :
 [[
    let induction_ltof2 F a = indrec a
    where rec indrec a = F a indrec;;
@@ -78,7 +78,7 @@ Proof.
   unfold ltof in |- *; intros b ltfafb.
   apply IHn.
   apply lt_le_trans with (f a); auto with arith.
-Defined. 
+Defined.
 
 Theorem induction_gtof1 :
   forall P:A -> Set,
@@ -262,7 +262,7 @@ Unset Implicit Arguments.
 
 (** [n]th iteration of the function [f] *)
 
-Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
+Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) : A :=
   match n with
     | O => x
     | S n' => f (iter_nat n' A f x)
@@ -271,8 +271,8 @@ Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
 Theorem iter_nat_plus :
   forall (n m:nat) (A:Type) (f:A -> A) (x:A),
     iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
-Proof.    
+Proof.
   simple induction n;
     [ simpl in |- *; auto with arith
-      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].  
+      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].
 Qed.
diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget
new file mode 100644
index 00000000..c3f29d21
--- /dev/null
+++ b/theories/Arith/vo.itarget
@@ -0,0 +1,23 @@
+Arith_base.vo
+Arith.vo
+Between.vo
+Bool_nat.vo
+Compare_dec.vo
+Compare.vo
+Div2.vo
+EqNat.vo
+Euclid.vo
+Even.vo
+Factorial.vo
+Gt.vo
+Le.vo
+Lt.vo
+Max.vo
+Minus.vo
+Min.vo
+Mult.vo
+Peano_dec.vo
+Plus.vo
+Wf_nat.vo
+NatOrderedType.vo
+MinMax.vo