Merge commit 'upstream/8.1.gamma' into 8.1

21 files changed, 1148 insertions, 1039 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 59d9b2b1..be065f1d 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -6,15 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Arith.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Arith.v 9302 2006-10-27 21:21:17Z barras $ i*)
 
-Require Export Le.
-Require Export Lt.
-Require Export Plus.
-Require Export Gt.
-Require Export Minus.
-Require Export Mult.
-Require Export Between.
-Require Export Peano_dec.
-Require Export Compare_dec.
-Require Export Factorial.
+Require Export Arith_base.
+Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
new file mode 100644
index 00000000..b076de2a
--- /dev/null
+++ b/theories/Arith/Arith_base.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Le.
+Require Export Lt.
+Require Export Plus.
+Require Export Gt.
+Require Export Minus.
+Require Export Mult.
+Require Export Between.
+Require Export Peano_dec.
+Require Export Compare_dec.
+Require Export Factorial.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 7680997d..2e9472c4 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 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Between.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Le.
 Require Import Lt.
@@ -16,174 +16,174 @@ Open Local Scope nat_scope.
 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.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-Hint Resolve bet_eq: arith v62.
-
-Lemma between_le : forall k l, between k l -> k <= l.
-Proof.
-induction 1; auto with arith.
-Qed.
-Hint Immediate between_le: arith v62.
-
-Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
-Proof.
-induction 1.
-intros; absurd (S k <= k); auto with arith.
-destruct H; auto with arith.
-Qed.
-Hint Resolve between_Sk_l: arith v62.
-
-Lemma between_restr :
- forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-Inductive exists_between k : nat -> Prop :=
-  | exists_S : forall l, exists_between k l -> exists_between k (S l)
-  | exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
-
-Hint Constructors exists_between: arith v62.
-
-Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-Lemma exists_lt : forall k l, exists_between k l -> k < l.
-Proof exists_le_S.
-Hint Immediate exists_le_S exists_lt: arith v62.
-
-Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
-Proof.
-intros; apply le_S_n; auto with arith.
-Qed.
-Hint Immediate exists_S_le: arith v62.
-
-Definition in_int p q r := p <= r /\ r < q.
-
-Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
-Proof.
-red in |- *; auto with arith.
-Qed.
-Hint Resolve in_int_intro: arith v62.
-
-Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
-Proof.
-induction 1; intros.
-apply le_lt_trans with r; auto with arith.
-Qed.
-
-Lemma in_int_p_Sq :
- forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat.
-Proof.
-induction 1; intros.
-elim (le_lt_or_eq r q); auto with arith.
-Qed.
-
-Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r.
-Proof.
-induction 1; auto with arith.
-Qed.
-Hint Resolve in_int_S: arith v62.
-
-Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
-Proof.
-induction 1; auto with arith.
-Qed.
-Hint Immediate in_int_Sp_q: arith v62.
-
-Lemma between_in_int :
- forall k l, between k l -> forall r, in_int k l r -> P r.
-Proof.
-induction 1; intros.
-absurd (k < k); auto with arith.
-apply in_int_lt with r; auto with arith.
-elim (in_int_p_Sq k l r); intros; auto with arith.
-rewrite H2; trivial with arith.
-Qed.
-
-Lemma in_int_between :
- forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l.
-Proof.
-induction 1; auto with arith.
-Qed.
-
-Lemma exists_in_int :
- forall k l, exists_between k l ->  exists2 m : nat, in_int k l m & Q m.
-Proof.
-induction 1.
-case IHexists_between; intros p inp Qp; exists p; auto with arith.
-exists l; auto with arith.
-Qed.
-
-Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l.
-Proof.
-destruct 1; intros.
-elim H0; auto with arith.
-Qed.
-
-Lemma between_or_exists :
- forall k l,
-   k <= l ->
-   (forall n:nat, in_int k l n -> P n \/ Q n) ->
-   between k l \/ exists_between k l.
-Proof.
-induction 1; intros; auto with arith.
-elim IHle; intro; auto with arith.
-elim (H0 m); auto with arith.
-Qed.
-
-Lemma between_not_exists :
- forall k l,
-   between k l ->
-   (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
-Proof.
-induction 1; red in |- *; intros.
-absurd (k < k); auto with arith.
-absurd (Q l); auto with arith.
-elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'.
-replace l with l'; auto with arith.
-elim inl'; intros.
-elim (le_lt_or_eq l' l); auto with arith; intros.
-absurd (exists_between k l); auto with arith.
-apply in_int_exists with l'; auto with arith.
-Qed.
-
-Inductive P_nth (init:nat) : nat -> nat -> Prop :=
-  | nth_O : P_nth init init 0
-  | nth_S :
+  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.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  Hint Resolve bet_eq: arith v62.
+
+  Lemma between_le : forall k l, between k l -> k <= l.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+  Hint Immediate between_le: arith v62.
+
+  Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
+  Proof.
+    intros k l H; induction H as [|l H].
+    intros; absurd (S k <= k); auto with arith.
+    destruct H; auto with arith.
+  Qed.
+  Hint Resolve between_Sk_l: arith v62.
+
+  Lemma between_restr :
+    forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  Inductive exists_between k : nat -> Prop :=
+    | exists_S : forall l, exists_between k l -> exists_between k (S l)
+    | exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
+
+  Hint Constructors exists_between: arith v62.
+
+  Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  Lemma exists_lt : forall k l, exists_between k l -> k < l.
+  Proof exists_le_S.
+  Hint Immediate exists_le_S exists_lt: arith v62.
+
+  Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
+  Proof.
+    intros; apply le_S_n; auto with arith.
+  Qed.
+  Hint Immediate exists_S_le: arith v62.
+
+  Definition in_int p q r := p <= r /\ r < q.
+
+  Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
+  Proof.
+    red in |- *; auto with arith.
+  Qed.
+  Hint Resolve in_int_intro: arith v62.
+
+  Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
+  Proof.
+    induction 1; intros.
+    apply le_lt_trans with r; auto with arith.
+  Qed.
+
+  Lemma in_int_p_Sq :
+    forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat.
+  Proof.
+    induction 1; intros.
+    elim (le_lt_or_eq r q); auto with arith.
+  Qed.
+
+  Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+  Hint Resolve in_int_S: arith v62.
+
+  Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+  Hint Immediate in_int_Sp_q: arith v62.
+
+  Lemma between_in_int :
+    forall k l, between k l -> forall r, in_int k l r -> P r.
+  Proof.
+    induction 1; intros.
+    absurd (k < k); auto with arith.
+    apply in_int_lt with r; auto with arith.
+    elim (in_int_p_Sq k l r); intros; auto with arith.
+    rewrite H2; trivial with arith.
+  Qed.
+
+  Lemma in_int_between :
+    forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l.
+  Proof.
+    induction 1; auto with arith.
+  Qed.
+
+  Lemma exists_in_int :
+    forall k l, exists_between k l ->  exists2 m : nat, in_int k l m & Q m.
+  Proof.
+    induction 1.
+    case IHexists_between; intros p inp Qp; exists p; auto with arith.
+    exists l; auto with arith.
+  Qed.
+
+  Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l.
+  Proof.
+    destruct 1; intros.
+    elim H0; auto with arith.
+  Qed.
+
+  Lemma between_or_exists :
+    forall k l,
+      k <= l ->
+      (forall n:nat, in_int k l n -> P n \/ Q n) ->
+      between k l \/ exists_between k l.
+  Proof.
+    induction 1; intros; auto with arith.
+    elim IHle; intro; auto with arith.
+    elim (H0 m); auto with arith.
+  Qed.
+
+  Lemma between_not_exists :
+    forall k l,
+      between k l ->
+      (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
+  Proof.
+    induction 1; red in |- *; intros.
+    absurd (k < k); auto with arith.
+    absurd (Q l); auto with arith.
+    elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'.
+    replace l with l'; auto with arith.
+    elim inl'; intros.
+    elim (le_lt_or_eq l' l); auto with arith; intros.
+    absurd (exists_between k l); auto with arith.
+    apply in_int_exists with l'; auto with arith.
+  Qed.
+
+  Inductive P_nth (init:nat) : nat -> nat -> Prop :=
+    | nth_O : P_nth init init 0
+    | nth_S :
       forall k l (n:nat),
-        P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n).
+	P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n).
 
-Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
-Proof.
-induction 1; intros; auto with arith.
-apply le_trans with (S k); auto with arith.
-Qed.
+  Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
+  Proof.
+    induction 1; intros; auto with arith.
+    apply le_trans with (S k); auto with arith.
+  Qed.
 
-Definition eventually (n:nat) :=  exists2 k : nat, k <= n & Q k.
+  Definition eventually (n:nat) :=  exists2 k : nat, k <= n & Q k.
 
-Lemma event_O : eventually 0 -> Q 0.
-Proof.
-induction 1; intros.
-replace 0 with x; auto with arith.
-Qed.
+  Lemma event_O : eventually 0 -> Q 0.
+  Proof.
+    induction 1; intros.
+    replace 0 with x; auto with arith.
+  Qed.
 
 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. 
-Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
\ No newline at end of file
+Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index b11f0517..06898658 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -6,21 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Compare.v 9302 2006-10-27 21:21:17Z barras $ i*)
 
 (** Equality is decidable on [nat] *)
+
 Open Local Scope nat_scope.
 
-(*
-Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p).
-Proof sym_not_eq.
-Hints Immediate not_eq_sym : arith.
-*)
 Notation not_eq_sym := sym_not_eq.
 
 Implicit Types m n p q : nat.
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import Peano_dec.
 Require Import Compare_dec.
 
@@ -41,17 +37,17 @@ Proof le_lt_or_eq.
 
 (* By special request of G. Kahn - Used in Group Theory *)
 Lemma discrete_nat :
- forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))).
+  forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))).
 Proof.
-intros m n H.
-lapply (lt_le_S m n); auto with arith.
-intro H'; lapply (le_lt_or_eq (S m) n); auto with arith.
-induction 1; auto with arith.
-right; exists (n - S (S m)); simpl in |- *.
-rewrite (plus_comm m (n - S (S m))).
-rewrite (plus_n_Sm (n - S (S m)) m).
-rewrite (plus_n_Sm (n - S (S m)) (S m)).
-rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith.
+  intros m n H.
+  lapply (lt_le_S m n); auto with arith.
+  intro H'; lapply (le_lt_or_eq (S m) n); auto with arith.
+  induction 1; auto with arith.
+  right; exists (n - S (S m)); simpl in |- *.
+  rewrite (plus_comm m (n - S (S m))).
+  rewrite (plus_n_Sm (n - S (S m)) m).
+  rewrite (plus_n_Sm (n - S (S m)) (S m)).
+  rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith.
 Qed.
 
 Require Export Wf_nat.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index d2eead86..e6dc7c46 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 8733 2006-04-25 22:52:18Z letouzey $ i*)
+(*i $Id: Compare_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Le.
 Require Import Lt.
@@ -17,109 +17,113 @@ Open Local Scope nat_scope.
 
 Implicit Types m n x y : nat.
 
-Definition zerop : forall n, {n = 0} + {0 < n}.
-destruct n; auto with arith.
+Definition zerop n : {n = 0} + {0 < n}.
+  destruct n; auto with arith.
 Defined.
 
-Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}.
-Proof.
-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 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.
 Defined.
 
-Lemma gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}.
-Proof lt_eq_lt_dec.
+Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
+  exact lt_eq_lt_dec.
+Defined.
 
-Lemma le_lt_dec : forall n m, {n <= m} + {m < n}.
-Proof.
-induction n.
-auto with arith.
-induction m.
-auto with arith.
-elim (IHn m); auto with arith.
+Definition le_lt_dec n m : {n <= m} + {m < n}.
+  induction n.
+  auto with arith.
+  induction m.
+  auto with arith.
+  elim (IHn m); auto with arith.
 Defined.
 
-Definition le_le_S_dec : forall n m, {n <= m} + {S m <= n}.
-Proof.
-exact le_lt_dec.
+Definition le_le_S_dec n m : {n <= m} + {S m <= n}.
+  exact le_lt_dec.
 Defined.
 
-Definition le_ge_dec : forall n m, {n <= m} + {n >= m}.
-Proof.
-intros; elim (le_lt_dec n m); auto with arith.
+Definition le_ge_dec n m : {n <= m} + {n >= m}.
+  intros; elim (le_lt_dec n m); auto with arith.
 Defined.
 
-Definition le_gt_dec : forall n m, {n <= m} + {n > m}.
-Proof.
-exact le_lt_dec.
+Definition le_gt_dec n m : {n <= m} + {n > m}.
+  exact le_lt_dec.
 Defined.
 
-Definition le_lt_eq_dec : forall n m, n <= m -> {n < m} + {n = m}.
-Proof.
-intros; elim (lt_eq_lt_dec n m); auto with arith.
-intros; absurd (m < n); auto with arith.
+Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
+  intros; elim (lt_eq_lt_dec n m); auto with arith.
+  intros; absurd (m < n); auto with arith.
 Defined.
 
 (** Proofs of decidability *)
 
 Theorem dec_le : forall n m, decidable (n <= m).
-intros x y; unfold decidable in |- *; elim (le_gt_dec x y);
- [ auto with arith | intro; right; apply gt_not_le; assumption ].
+Proof.
+  intros x y; unfold decidable in |- *; elim (le_gt_dec x y);
+    [ auto with arith | intro; right; apply gt_not_le; assumption ].
 Qed.
 
 Theorem dec_lt : forall n m, decidable (n < m).
-intros x y; unfold lt in |- *; apply dec_le.
+Proof.
+  intros x y; unfold lt in |- *; apply dec_le.
 Qed.
 
 Theorem dec_gt : forall n m, decidable (n > m).
-intros x y; unfold gt in |- *; apply dec_lt.
+Proof.
+  intros x y; unfold gt in |- *; apply dec_lt.
 Qed.
 
 Theorem dec_ge : forall n m, decidable (n >= m).
-intros x y; unfold ge in |- *; apply dec_le.
+Proof.
+  intros x y; unfold ge in |- *; apply dec_le.
 Qed.
 
 Theorem not_eq : forall n m, n <> m -> n < m \/ m < n.
-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 ].
+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 ].
 Qed.
 
 
 Theorem not_le : forall n m, ~ n <= m -> n > m.
-intros x y H; elim (le_gt_dec x y);
- [ intros H1; absurd (x <= y); assumption | trivial with arith ].
+Proof.
+  intros x y H; elim (le_gt_dec x y);
+    [ intros H1; absurd (x <= y); assumption | trivial with arith ].
 Qed.
 
 Theorem not_gt : forall n m, ~ n > m -> n <= m.
-intros x y H; elim (le_gt_dec x y);
- [ trivial with arith | intros H1; absurd (x > y); assumption ].
+Proof.
+  intros x y H; elim (le_gt_dec x y);
+    [ trivial with arith | intros H1; absurd (x > y); assumption ].
 Qed.
 
 Theorem not_ge : forall n m, ~ n >= m -> n < m.
-intros x y H; exact (not_le y x H).
+Proof.
+  intros x y H; exact (not_le y x H).
 Qed.
 
 Theorem not_lt : forall n m, ~ n < m -> n >= m.
-intros x y H; exact (not_gt y x H). 
+Proof.
+  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
- end.
+  match lt_eq_lt_dec n m with 
+    | inleft (left _) => Lt
+    | inleft (right _) => Eq
+    | inright _ => Gt
+  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.
+  unfold nat_compare; intros.
+  simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto.
 Qed.
 
 Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m.
@@ -188,11 +192,11 @@ Qed.
 
 Fixpoint leb (m:nat) : nat -> bool :=
   match m with
-  | O => fun _:nat => true
-  | S m' =>
+    | O => fun _:nat => true
+    | S m' =>
       fun n:nat => match n with
-                   | O => false
-                   | S n' => leb m' n'
+                     | O => false
+                     | S n' => leb m' n'
                    end
   end.
 
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index 9011cee3..1dec34e2 100644
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Div.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Div.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** Euclidean division *)
 
@@ -20,45 +20,45 @@ Require Compare_dec.
 Implicit Variables Type n,a,b,q,r:nat.
 
 Fixpoint inf_dec [n:nat] : nat->bool :=
-      [m:nat] Cases n m of
-                  O     _     => true
-              | (S n')  O     => false
-              | (S n') (S m') => (inf_dec n' m')
-             end.
+  [m:nat] Cases n m of
+            O     _     => true
+            | (S n')  O     => false
+            | (S n') (S m') => (inf_dec n' m')
+          end.
 
 Theorem div1 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
-Realizer Fix div1 {div1/2: nat->nat->diveucl :=
-  [b,a]Cases a of
-         O     => (O,O)
-       | (S n) =>
-           let (q,r) = (div1 b n) in
-             if (le_gt_dec b (S r)) then ((S q),O)
-	     else (q,(S r))
-       end}.
-Program_all.
-Rewrite e.
-Replace b with (S r).
-Simpl.
-Elim plus_n_O; Auto with arith.
-Apply le_antisym; Auto with arith.
-Elim plus_n_Sm; Auto with arith.
+  Realizer Fix div1 {div1/2: nat->nat->diveucl :=
+    [b,a]Cases a of
+           O     => (O,O)
+	   | (S n) =>
+             let (q,r) = (div1 b n) in
+               if (le_gt_dec b (S r)) then ((S q),O)
+		 else (q,(S r))
+	 end}.
+  Program_all.
+  Rewrite e.
+  Replace b with (S r).
+  Simpl.
+  Elim plus_n_O; Auto with arith.
+  Apply le_antisym; Auto with arith.
+  Elim plus_n_Sm; Auto with arith.
 Qed.
 
 Theorem div2 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
-Realizer Fix div1 {div1/2: nat->nat->diveucl :=
-  [b,a]Cases a of
-         O     => (O,O)
-       | (S n) =>
-           let (q,r) = (div1 b n) in
-             if (inf_dec b (S r)) :: :: { {(le b (S r))}+{(gt b (S r))} }
-             then ((S q),O)
-	     else (q,(S r))
-       end}.
-Program_all.
-Rewrite e.
-Replace b with (S r).
-Simpl.
-Elim plus_n_O; Auto with arith.
-Apply le_antisym; Auto with arith.
-Elim plus_n_Sm; Auto with arith.
+  Realizer Fix div1 {div1/2: nat->nat->diveucl :=
+    [b,a]Cases a of
+           O     => (O,O)
+	   | (S n) =>
+             let (q,r) = (div1 b n) in
+               if (inf_dec b (S r)) :: :: { {(le b (S r))}+{(gt b (S r))} }
+		 then ((S q),O)
+		 else (q,(S r))
+	 end}.
+  Program_all.
+  Rewrite e.
+  Replace b with (S r).
+  Simpl.
+  Elim plus_n_O; Auto with arith.
+  Apply le_antisym; Auto with arith.
+  Elim plus_n_Sm; Auto with arith.
 Qed.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index ca1f39af..c32759b2 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 8733 2006-04-25 22:52:18Z letouzey $ i*)
+(*i $Id: Div2.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Lt.
 Require Import Plus.
@@ -30,28 +30,30 @@ Fixpoint div2 n : nat :=
     useful to prove the corresponding induction principle *)
 
 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.
+  forall P:nat -> Prop,
+    P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
 Proof.
-intros.
-cut (forall n, P n /\ P (S n)).
-intros. elim (H2 n). auto with arith.
-
-induction n0. auto with arith.
-intros. elim IHn0; auto with arith.
+  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.
 
 (** [0 <n  =>  n/2 < n] *)
 
 Lemma lt_div2 : forall n, 0 < n -> div2 n < n.
 Proof.
-intro n. pattern n in |- *. apply ind_0_1_SS.
-intro. inversion H.
-auto with arith.
-intros. simpl in |- *.
-case (zerop n0).
-intro. rewrite e. auto with arith.
-auto with arith.
+  intro n. pattern n in |- *. 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.
 
 Hint Resolve lt_div2: arith.
@@ -59,27 +61,27 @@ Hint Resolve lt_div2: arith.
 (** Properties related to the parity *)
 
 Lemma even_odd_div2 :
- forall n,
-   (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+  forall n,
+    (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
 Proof.
-intro n. pattern n in |- *. apply ind_0_1_SS.
-(* n  = 0 *)
-split. split; auto with arith. 
-split. intro H. inversion H.
-intro H.  absurd (S (div2 0) = div2 1); auto with arith.
-(* n = 1 *)
-split. split. intro. inversion H. inversion H1.
-intro H.  absurd (div2 1 = div2 2).
-simpl in |- *. discriminate. assumption.
-split; auto with arith.
-(* n = (S (S n')) *)
-intros. decompose [and] H. unfold iff in H0, H1.
-decompose [and] H0. decompose [and] H1. clear H H0 H1.
-split; split; auto with arith.
-intro H. inversion H. inversion H1.
-change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
-intro H. inversion H. inversion H1.
-change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
+  intro n. pattern n in |- *. apply ind_0_1_SS.
+  (* n  = 0 *)
+  split. split; auto with arith. 
+  split. intro H. inversion H.
+  intro H.  absurd (S (div2 0) = div2 1); auto with arith.
+  (* n = 1 *)
+  split. split. intro. inversion H. inversion H1.
+  intro H.  absurd (div2 1 = div2 2).
+  simpl in |- *. discriminate. assumption.
+  split; auto with arith.
+  (* n = (S (S n')) *)
+  intros. decompose [and] H. unfold iff in H0, H1.
+  decompose [and] H0. decompose [and] H1. clear H H0 H1.
+  split; split; auto with arith.
+  intro H. inversion H. inversion H1.
+  change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
+  intro H. inversion H. inversion H1.
+  change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
 Qed.
 
 (** Specializations *)
@@ -106,39 +108,39 @@ Hint Unfold double: arith.
 
 Lemma double_S : forall n, double (S n) = S (S (double n)).
 Proof.
-intro. unfold double in |- *. simpl in |- *. auto with arith.
+  intro. unfold double in |- *. simpl in |- *. auto with arith.
 Qed.
 
 Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m.
 Proof.
-intros m n. unfold double in |- *.
-do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
-reflexivity.
+  intros m n. unfold double in |- *.
+  do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
+  reflexivity.
 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))).
+  forall n,
+    (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
 Proof.
-intro n. pattern n in |- *. 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. decompose [and] H. unfold iff in H0, H1.
-decompose [and] H0. decompose [and] H1. clear H H0 H1.
-split; split.
-intro H. inversion H. inversion H1.
-simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
-simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
-intro H. inversion H. inversion H1.
-simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
-simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+  intro n. pattern n in |- *. 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. decompose [and] H. unfold iff in H0, H1.
+  decompose [and] H0. decompose [and] H1. clear H H0 H1.
+  split; split.
+  intro H. inversion H. inversion H1.
+  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
+  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+  intro H. inversion H. inversion H1.
+  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
+  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
 Qed.
 
 
@@ -166,32 +168,32 @@ Hint Resolve even_double double_even odd_double double_odd: arith.
 
 Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
 Proof.
-intros n H. exists (div2 n). auto with arith.
+  intros n H. exists (div2 n). auto with arith.
 Qed.
 
 Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
 Proof.
-intros n H. exists (div2 n). auto with arith.
+  intros n H. exists (div2 n). auto with arith.
 Qed.
 
 (** 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.
+  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 : 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.
+  induction n.
+  simpl; auto.
+  simpl.
+  replace (n+S(n+0)) with (S (2*n)).
+  f_equal; auto.
+  simpl; auto with arith.
 Qed.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 09df9464..82d05e2c 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 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: EqNat.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** Equality on natural numbers *)
 
@@ -14,52 +14,66 @@ Open Local Scope nat_scope.
 
 Implicit Types m n x y : nat.
 
+(** * Propositional equality  *)
+
 Fixpoint eq_nat n m {struct n} : Prop :=
   match n, m with
-  | O, O => True
-  | O, S _ => False
-  | S _, O => False
-  | S n1, S m1 => eq_nat n1 m1
+    | O, O => True
+    | O, S _ => False
+    | S _, O => False
+    | S n1, S m1 => eq_nat n1 m1
   end.
 
 Theorem eq_nat_refl : forall n, eq_nat n n.
-induction n; simpl in |- *; auto.
+  induction n; simpl in |- *; auto.
 Qed.
 Hint Resolve eq_nat_refl: arith v62.
 
-Theorem eq_eq_nat : forall n m, n = m -> eq_nat n m.
-induction 1; trivial with arith.
+(** [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.
 Qed.
 Hint Immediate eq_eq_nat: arith v62.
 
-Theorem eq_nat_eq : forall n m, eq_nat n m -> n = m.
-induction n; induction m; simpl in |- *; contradiction || auto with arith.
+Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m.
+  induction n; induction m; simpl in |- *; contradiction || auto with arith.
 Qed.
 Hint Immediate eq_nat_eq: arith v62.
 
+Theorem eq_nat_is_eq : forall n m, eq_nat n m <-> n = m.
+Proof.
+  split; auto with arith.
+Qed.
+
 Theorem eq_nat_elim :
- forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
-intros; replace m with n; auto with arith.
+  forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
+Proof.
+  intros; replace m with n; auto with arith.
 Qed.
 
 Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.
-induction n.
-destruct m as [| n].
-auto with arith.
-intros; right; red in |- *; trivial with arith.
-destruct m as [| n0].
-right; red in |- *; auto with arith.
-intros.
-simpl in |- *.
-apply IHn.
+Proof.
+  induction n.
+  destruct m as [| n].
+  auto with arith.
+  intros; right; red in |- *; trivial with arith.
+  destruct m as [| n0].
+  right; red in |- *; auto with arith.
+  intros.
+  simpl in |- *.
+  apply IHn.
 Defined.
 
+
+(** * Boolean equality on [nat] *)
+
 Fixpoint beq_nat n m {struct n} : bool :=
   match n, m with
-  | O, O => true
-  | O, S _ => false
-  | S _, O => false
-  | S n1, S m1 => beq_nat n1 m1
+    | O, O => true
+    | O, S _ => false
+    | S _, O => false
+    | S n1, S m1 => beq_nat n1 m1
   end.
 
 Lemma beq_nat_refl : forall n, true = beq_nat n n.
@@ -71,7 +85,7 @@ Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y.
 Proof.
   double induction x y; simpl in |- *.
     reflexivity.
-    intros; discriminate H0.
-    intros; discriminate H0.
-    intros; case (H0 _ H1); reflexivity.
+    intros n H1 H2. discriminate H2.
+    intros n H1 H2. discriminate H2.
+    intros n H1 z H2 H3. case (H2 _ H3). reflexivity.
 Defined.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 23bc7cdb..3d6f1af5 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 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Euclid.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Mult.
 Require Import Compare_dec.
@@ -17,52 +17,55 @@ Open Local Scope nat_scope.
 Implicit Types a b n q r : nat.
 
 Inductive diveucl a b : Set :=
-    divex : forall q r, b > r -> a = q * b + r -> diveucl a b.
+  divex : forall q r, b > r -> a = q * b + r -> diveucl a b.
 
 
 Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n.
-intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
-elim (le_gt_dec b n).
-intro lebn.
-elim (H0 (n - b)); auto with arith.
-intros q r g e.
-apply divex with (S q) r; simpl in |- *; auto with arith.
-elim plus_assoc.
-elim e; auto with arith.
-intros gtbn.
-apply divex with 0 n; simpl in |- *; auto with arith.
+Proof.
+  intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
+  elim (le_gt_dec b n).
+  intro lebn.
+  elim (H0 (n - b)); auto with arith.
+  intros q r g e.
+  apply divex with (S q) r; simpl in |- *; auto with arith.
+  elim plus_assoc.
+  elim e; auto with arith.
+  intros gtbn.
+  apply divex with 0 n; simpl in |- *; auto with arith.
 Qed.
 
 Lemma quotient :
- forall n,
-   n > 0 ->
-   forall m:nat, {q : nat |  exists r : nat, m = q * n + r /\ n > r}.
-intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
-elim (le_gt_dec b n).
-intro lebn.
-elim (H0 (n - b)); auto with arith.
-intros q Hq; exists (S q).
-elim Hq; intros r Hr.
-exists r; simpl in |- *; elim Hr; intros.
-elim plus_assoc.
-elim H1; auto with arith.
-intros gtbn.
-exists 0; exists n; simpl in |- *; auto with arith.
+  forall n,
+    n > 0 ->
+    forall m:nat, {q : nat |  exists r : nat, m = q * n + r /\ n > r}.
+Proof.
+  intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
+  elim (le_gt_dec b n).
+  intro lebn.
+  elim (H0 (n - b)); auto with arith.
+  intros q Hq; exists (S q).
+  elim Hq; intros r Hr.
+  exists r; simpl in |- *; elim Hr; intros.
+  elim plus_assoc.
+  elim H1; auto with arith.
+  intros gtbn.
+  exists 0; exists n; simpl in |- *; auto with arith.
 Qed.
 
 Lemma modulo :
- forall n,
-   n > 0 ->
-   forall m:nat, {r : nat |  exists q : nat, m = q * n + r /\ n > r}.
-intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
-elim (le_gt_dec b n).
-intro lebn.
-elim (H0 (n - b)); auto with arith.
-intros r Hr; exists r.
-elim Hr; intros q Hq.
-elim Hq; intros; exists (S q); simpl in |- *.
-elim plus_assoc.
-elim H1; auto with arith.
-intros gtbn.
-exists n; exists 0; simpl in |- *; auto with arith.
-Qed.
\ No newline at end of file
+  forall n,
+    n > 0 ->
+    forall m:nat, {r : nat |  exists q : nat, m = q * n + r /\ n > r}.
+Proof.
+  intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
+  elim (le_gt_dec b n).
+  intro lebn.
+  elim (H0 (n - b)); auto with arith.
+  intros r Hr; exists r.
+  elim Hr; intros q Hq.
+  elim Hq; intros; exists (S q); simpl in |- *.
+  elim plus_assoc.
+  elim H1; auto with arith.
+  intros gtbn.
+  exists n; exists 0; simpl in |- *; auto with arith.
+Qed.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index cdbc86df..83c0ce17 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 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Even.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
@@ -16,6 +16,9 @@ Open Local Scope nat_scope.
 
 Implicit Types m n : nat.
 
+
+(** * Definition of [even] and [odd], and basic facts *) 
+
 Inductive even : nat -> Prop :=
   | even_O : even 0
   | even_S : forall n, odd n -> even (S n)
@@ -27,279 +30,285 @@ Hint Constructors odd: arith.
 
 Lemma even_or_odd : forall n, even n \/ odd n.
 Proof.
-induction n.
-auto with arith.
-elim IHn; auto with arith.
+  induction n.
+    auto with arith.
+    elim IHn; auto with arith.
 Qed.
 
 Lemma even_odd_dec : forall n, {even n} + {odd n}.
 Proof.
-induction n.
-auto with arith.
-elim IHn; auto with arith.
+  induction n.
+    auto with arith.
+    elim IHn; auto with arith.
 Qed.
 
 Lemma not_even_and_odd : forall n, even n -> odd n -> False.
 Proof.
-induction n.
-intros. inversion H0.
-intros. inversion H. inversion H0. auto with arith.
+  induction n.
+    intros even_0 odd_0. inversion odd_0.
+    intros even_Sn odd_Sn. inversion even_Sn. inversion odd_Sn. auto with arith.
 Qed.
 
+
+(** * Facts about [even] & [odd] wrt. [plus] *)
+
 Lemma even_plus_aux :
- forall n m,
-   (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
-   (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
+  forall 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.
-intros n; elim n; simpl in |- *; auto with arith.
-intros m; split; auto.
-split.
-intros H; right; split; auto with arith.
-intros H'; case H'; auto with arith.
-intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
-intros H; elim H; auto.
-split; auto with arith.
-intros H'; elim H'; auto with arith.
-intros H; elim H; auto.
-intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
-intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2;
- intros E3 E4; clear H'1 H'2.
-split; split.
-intros H'0; case E3.
-inversion H'0; auto.
-intros H; elim H; intros H0 H1; clear H; auto with arith.
-intros H; elim H; intros H0 H1; clear H; auto with arith.
-intros H'0; case H'0; intros C0; case C0; intros C1 C2.
-apply odd_S.
-apply E4; left; split; auto with arith.
-inversion C1; auto.
-apply odd_S.
-apply E4; right; split; auto with arith.
-inversion C1; auto.
-intros H'0.
-case E1.
-inversion H'0; auto.
-intros H; elim H; intros H0 H1; clear H; auto with arith.
-intros H; elim H; intros H0 H1; clear H; auto with arith.
-intros H'0; case H'0; intros C0; case C0; intros C1 C2.
-apply even_S.
-apply E2; left; split; auto with arith.
-inversion C1; auto.
-apply even_S.
-apply E2; right; split; auto with arith.
-inversion C1; auto.
+  intros n; elim n; simpl in |- *; auto with arith.
+  intros m; split; auto.
+  split.
+  intros H; right; split; auto with arith.
+  intros H'; case H'; auto with arith.
+  intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
+  intros H; elim H; auto.
+  split; auto with arith.
+  intros H'; elim H'; auto with arith.
+  intros H; elim H; auto.
+  intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
+  intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2;
+    intros E3 E4; clear H'1 H'2.
+  split; split.
+  intros H'0; case E3.
+  inversion H'0; auto.
+  intros H; elim H; intros H0 H1; clear H; auto with arith.
+  intros H; elim H; intros H0 H1; clear H; auto with arith.
+  intros H'0; case H'0; intros C0; case C0; intros C1 C2.
+  apply odd_S.
+  apply E4; left; split; auto with arith.
+  inversion C1; auto.
+  apply odd_S.
+  apply E4; right; split; auto with arith.
+  inversion C1; auto.
+  intros H'0.
+  case E1.
+  inversion H'0; auto.
+  intros H; elim H; intros H0 H1; clear H; auto with arith.
+  intros H; elim H; intros H0 H1; clear H; auto with arith.
+  intros H'0; case H'0; intros C0; case C0; intros C1 C2.
+  apply even_S.
+  apply E2; left; split; auto with arith.
+  inversion C1; auto.
+  apply even_S.
+  apply E2; right; split; auto with arith.
+  inversion C1; auto.
 Qed.
  
 Lemma even_even_plus : forall n m, even n -> even m -> even (n + m).
 Proof.
-intros n m; case (even_plus_aux n m).
-intros H H0; case H0; auto.
+  intros n m; case (even_plus_aux n m).
+  intros H H0; case H0; auto.
 Qed.
  
 Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
 Proof.
-intros n m; case (even_plus_aux n m).
-intros H H0; case H0; auto.
+  intros n m; case (even_plus_aux n m).
+  intros H H0; case H0; auto.
 Qed.
- 
+
 Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'0.
-intros H'1; case H'1; auto.
-intros H0; elim H0; auto.
-intros H0 H1 H2; case (not_even_and_odd n); auto.
-case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'0.
+  intros H'1; case H'1; auto.
+  intros H0; elim H0; auto.
+  intros H0 H1 H2; case (not_even_and_odd n); auto.
+  case H0; auto.
 Qed.
  
 Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'0.
-intros H'1; case H'1; auto.
-intros H0; elim H0; auto.
-intros H0 H1 H2; case (not_even_and_odd m); auto.
-case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'0.
+  intros H'1; case H'1; auto.
+  intros H0; elim H0; auto.
+  intros H0 H1 H2; case (not_even_and_odd m); auto.
+  case H0; auto.
 Qed.
- 
+
 Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'0.
-intros H'1; case H'1; auto.
-intros H0 H1 H2; case (not_even_and_odd n); auto.
-case H0; auto.
-intros H0; case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'0.
+  intros H'1; case H'1; auto.
+  intros H0 H1 H2; case (not_even_and_odd n); auto.
+  case H0; auto.
+  intros H0; case H0; auto.
 Qed.
- 
+
 Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'0.
-intros H'1; case H'1; auto.
-intros H0 H1 H2; case (not_even_and_odd m); auto.
-case H0; auto.
-intros H0; case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'0.
+  intros H'1; case H'1; auto.
+  intros H0 H1 H2; case (not_even_and_odd m); auto.
+  case H0; auto.
+  intros H0; case H0; auto.
 Qed.
 Hint Resolve even_even_plus odd_even_plus: arith.
- 
+
 Lemma odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
 Proof.
-intros n m; case (even_plus_aux n m).
-intros H; case H; auto.
+  intros n m; case (even_plus_aux n m).
+  intros H; case H; auto.
 Qed.
  
 Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m).
 Proof.
-intros n m; case (even_plus_aux n m).
-intros H; case H; auto.
+  intros n m; case (even_plus_aux n m).
+  intros H; case H; auto.
 Qed.
  
 Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'.
-intros H'1; case H'1; auto.
-intros H0 H1 H2; case (not_even_and_odd m); auto.
-case H0; auto.
-intros H0; case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'.
+  intros H'1; case H'1; auto.
+  intros H0 H1 H2; case (not_even_and_odd m); auto.
+  case H0; auto.
+  intros H0; case H0; auto.
 Qed.
  
 Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'.
-intros H'1; case H'1; auto.
-intros H0; case H0; auto.
-intros H0 H1 H2; case (not_even_and_odd n); auto.
-case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'.
+  intros H'1; case H'1; auto.
+  intros H0; case H0; auto.
+  intros H0 H1 H2; case (not_even_and_odd n); auto.
+  case H0; auto.
 Qed.
  
 Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'.
-intros H'1; case H'1; auto.
-intros H0; case H0; auto.
-intros H0 H1 H2; case (not_even_and_odd m); auto.
-case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'.
+  intros H'1; case H'1; auto.
+  intros H0; case H0; auto.
+  intros H0 H1 H2; case (not_even_and_odd m); auto.
+  case H0; auto.
 Qed.
- 
+
 Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m.
 Proof.
-intros n m H; case (even_plus_aux n m).
-intros H' H'0; elim H'.
-intros H'1; case H'1; auto.
-intros H0 H1 H2; case (not_even_and_odd n); auto.
-case H0; auto.
-intros H0; case H0; auto.
+  intros n m H; case (even_plus_aux n m).
+  intros H' H'0; elim H'.
+  intros H'1; case H'1; auto.
+  intros H0 H1 H2; case (not_even_and_odd n); auto.
+  case H0; auto.
+  intros H0; case H0; auto.
 Qed.
 Hint Resolve odd_plus_l odd_plus_r: arith.
- 
+
+
+(** * 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).
+  forall n m,
+    (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
 Proof.
-intros n; elim n; simpl in |- *; 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.
+  intros n; elim n; simpl in |- *; 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_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.
+  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.
-intros H H0; case H0; auto.
+  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_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.
+  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_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.
+  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 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.
+  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'.
-case (even_mult_aux n m).
-intros H'1 H'2; elim H'1.
-intros H'3; elim H'3; auto.
+  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 : 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.
+  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.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 2767f9f0..5e2f491a 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 6338 2004-11-22 09:10:51Z gregoire $ i*)
+(*i $Id: Factorial.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Plus.
 Require Import Mult.
@@ -17,34 +17,34 @@ Open Local Scope nat_scope.
 
 Boxed Fixpoint fact (n:nat) : nat :=
   match n with
-  | O => 1
-  | S n => S n * fact n
+    | O => 1
+    | S n => S n * fact n
   end.
 
 Arguments Scope fact [nat_scope].
 
 Lemma lt_O_fact : forall n:nat, 0 < fact n.
 Proof.
-simple induction n; unfold lt in |- *; simpl in |- *; auto with arith.
+  simple induction n; unfold lt in |- *; simpl in |- *; auto with arith.
 Qed.
 
 Lemma fact_neq_0 : forall n:nat, fact n <> 0.
 Proof.
-intro.
-apply sym_not_eq.
-apply lt_O_neq.
-apply lt_O_fact.
+  intro.
+  apply sym_not_eq.
+  apply lt_O_neq.
+  apply lt_O_fact.
 Qed.
 
 Lemma fact_le : forall n m:nat, 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.
+  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.
 Qed.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 90f893a3..5b1ee1b2 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -6,7 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Gt.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Gt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+
+(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
+<<
+Definition gt (n m:nat) := m < n.
+>>
+*)
 
 Require Import Le.
 Require Import Lt.
@@ -15,7 +21,7 @@ Open Local Scope nat_scope.
 
 Implicit Types m n p : nat.
 
-(** Order and successor *)
+(** * Order and successor *)
 
 Theorem gt_Sn_O : forall n, S n > 0.
 Proof.
@@ -52,20 +58,20 @@ Proof.
 Qed.
 Hint Immediate gt_pred: arith v62.
 
-(** Irreflexivity *)
+(** * Irreflexivity *)
 
 Lemma gt_irrefl : forall n, ~ n > n.
 Proof lt_irrefl.
 Hint Resolve gt_irrefl: arith v62.
 
-(** Asymmetry *)
+(** * 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.
 
-(** Relating strict and large orders *)
+(** * Relating strict and large orders *)
 
 Lemma le_not_gt : forall n m, n <= m -> ~ n > m.
 Proof le_not_lt.
@@ -102,7 +108,7 @@ Proof.
 Qed.
 Hint Resolve le_gt_S: arith v62.
 
-(** Transitivity *)
+(** * Transitivity *)
 
 Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p.
 Proof.
@@ -127,14 +133,14 @@ Qed.
 
 Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
 
-(** Comparison to 0 *)
+(** * Comparison to 0 *)
 
 Theorem gt_O_eq : forall n, n > 0 \/ 0 = n.
 Proof.
   intro n; apply gt_S; auto with arith.
 Qed.
 
-(** Simplification and compatibility *)
+(** * Simplification and compatibility *)
 
 Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m.
 Proof.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index e95ef408..e8b9e6be 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -6,108 +6,124 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Le.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Le.v 9245 2006-10-17 12:53:34Z notin $ i*)
+
+(** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
+<<
+Inductive le (n:nat) : nat -> Prop :=
+  | le_n : n <= n
+  | le_S : forall m:nat, n <= m -> n <= S m
+
+where "n <= m" := (le n m) : nat_scope.
+>>
+ *)
 
-(** Order on natural numbers *)
 Open Local Scope nat_scope.
 
 Implicit Types m n p : nat.
 
-(** Reflexivity *)
+(** * [le] is a pre-order *)
 
+(** Reflexivity *)
 Theorem le_refl : forall n, n <= n.
 Proof.
-exact le_n.
+  exact le_n.
 Qed.
 
 (** 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.
 
-(** Order, successor and predecessor *)
+(** * Properties of [le] w.r.t. successor, predecessor and 0 *)
 
-Theorem le_n_S : forall n m, n <= m -> S n <= S m.
+(** Comparison to 0 *)
+
+Theorem le_O_n : forall n, 0 <= n.
 Proof.
-  induction 1; auto.
+  induction n; auto.
 Qed.
 
-Theorem le_n_Sn : forall n, n <= S n.
+Theorem le_Sn_O : forall n, ~ S n <= 0.
 Proof.
-  auto.
+  red in |- *; intros n H.
+  change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
 Qed.
 
-Theorem le_O_n : forall n, 0 <= n.
+Hint Resolve le_O_n le_Sn_O: arith v62.
+
+Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n.
 Proof.
-  induction n; auto.
+  induction n; auto with arith.
+  intro; contradiction le_Sn_O with n.
 Qed.
+Hint Immediate le_n_O_eq: arith v62.
 
-Hint Resolve le_n_S le_n_Sn le_O_n le_n_S: arith v62.
 
-Theorem le_pred_n : forall n, pred n <= n.
+(** [le] and successor *)
+
+Theorem le_n_S : forall n m, n <= m -> S n <= S m.
 Proof.
-induction n; auto with arith.
+  induction 1; auto.
 Qed.
-Hint Resolve le_pred_n: arith v62.
+
+Theorem le_n_Sn : forall n, n <= S n.
+Proof.
+  auto.
+Qed.
+
+Hint Resolve le_n_S le_n_Sn : arith v62.
 
 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.
+  intros n m H; apply le_trans with (S n); auto with arith.
 Qed.
 Hint Immediate le_Sn_le: arith v62.
 
 Theorem le_S_n : forall n m, S n <= S m -> n <= m.
 Proof.
-intros n m H; change (pred (S n) <= pred (S m)) in |- *.
-destruct H; simpl; auto with arith.
+  intros n m H; change (pred (S n) <= pred (S m)) in |- *.
+  destruct H; simpl; auto with arith.
 Qed.
 Hint Immediate le_S_n: arith v62.
 
-Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
+Theorem le_Sn_n : forall n, ~ S n <= n.
 Proof.
-destruct n; simpl; auto with arith.
-destruct m; simpl; auto with arith.
+  induction n; auto with arith.
 Qed.
+Hint Resolve le_Sn_n: arith v62.
 
-(** Comparison to 0 *)
+(** [le] and predecessor *)
 
-Theorem le_Sn_O : forall n, ~ S n <= 0.
+Theorem le_pred_n : forall n, pred n <= n.
 Proof.
-red in |- *; intros n H.
-change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
+  induction n; auto with arith.
 Qed.
-Hint Resolve le_Sn_O: arith v62.
+Hint Resolve le_pred_n: arith v62.
 
-Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n.
+Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
-induction n; auto with arith.
-intro; contradiction le_Sn_O with n.
+  destruct n; simpl; auto with arith.
+  destruct m; simpl; auto with arith.
 Qed.
-Hint Immediate le_n_O_eq: arith v62.
 
-(** Negative properties *)
-
-Theorem le_Sn_n : forall n, ~ S n <= n.
-Proof.
-induction n; auto with arith.
-Qed.
-Hint Resolve le_Sn_n: arith v62.
 
+(** * [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 [| m0 H]; auto with arith.
-intros H1.
-absurd (S m0 <= m0); auto with arith.
-apply le_trans with n; auto with arith.
+  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 *)
+
+(** * A different elimination principle for the order on natural numbers *)
 
 Lemma le_elim_rel :
  forall P:nat -> nat -> Prop,
@@ -115,7 +131,7 @@ 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.
\ No newline at end of file
+  induction n; auto with arith.
+  intros m Le.
+  elim Le; auto with arith.
+Qed.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index eeb4e35e..94cf3793 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -6,86 +6,93 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Lt.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Lt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+
+(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
+<<
+Definition lt (n m:nat) := S n <= m.
+Infix "<" := lt : nat_scope.
+>>
+*)
 
 Require Import Le.
 Open Local Scope nat_scope.
 
 Implicit Types m n p : nat.
 
-(** Irreflexivity *)
+(** * Irreflexivity *)
 
 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.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Immediate lt_le_S: arith v62.
 
 Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Immediate lt_n_Sm_le: arith v62.
 
 Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Immediate le_lt_n_Sm: arith v62.
 
 Theorem le_not_lt : forall n m, n <= m -> ~ m < n.
 Proof.
-induction 1; auto with arith.
+  induction 1; auto with arith.
 Qed.
 
 Theorem lt_not_le : forall n m, n < m -> ~ m <= n.
 Proof.
-red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt).
+  red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt).
 Qed.
 Hint Immediate le_not_lt lt_not_le: arith v62.
 
-(** Asymmetry *)
+(** * Asymmetry *)
 
 Theorem lt_asym : forall n m, n < m -> ~ m < n.
 Proof.
-induction 1; auto with arith.
+  induction 1; auto with arith.
 Qed.
 
-(** Order and successor *)
+(** * Order and successor *)
 
 Theorem lt_n_Sn : forall n, n < S n.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Resolve lt_n_Sn: arith v62.
 
 Theorem lt_S : forall n m, n < m -> n < S m.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Resolve lt_S: arith v62.
 
 Theorem lt_n_S : forall n m, n < m -> S n < S m.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Resolve lt_n_S: arith v62.
 
 Theorem lt_S_n : forall n m, S n < S m -> n < m.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Immediate lt_S_n: arith v62.
 
 Theorem lt_O_Sn : forall n, 0 < S n.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Resolve lt_O_Sn: arith v62.
 
@@ -93,7 +100,7 @@ Theorem lt_n_O : forall n, ~ n < 0.
 Proof le_Sn_O.
 Hint Resolve lt_n_O: arith v62.
 
-(** Predecessor *)
+(** * Predecessor *)
 
 Lemma S_pred : forall n m, m < n -> n = S (pred n).
 Proof.
@@ -111,65 +118,65 @@ destruct 1; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve lt_pred_n_n: arith v62.
 
-(** Transitivity properties *)
+(** * Transitivity properties *)
 
 Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
 Proof.
-induction 2; auto with arith.
+  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.
+  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.
+  induction 2; auto with arith.
 Qed.
 
 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62.
 
-(** Large = strict or equal *)
+(** * Large = strict or equal *)
 
 Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m.
 Proof.
-induction 1; auto with arith.
+  induction 1; auto with arith.
 Qed.
 
 Theorem lt_le_weak : forall n m, n < m -> n <= m.
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Immediate lt_le_weak: arith v62.
 
-(** Dichotomy *)
+(** * Dichotomy *)
 
 Theorem le_or_lt : forall n m, n <= m \/ m < n.
 Proof.
-intros n m; pattern n, m in |- *; apply nat_double_ind; auto with arith.
-induction 1; auto with arith.
+  intros n m; pattern n, m in |- *; 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.
+  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 *)
+(** * Comparison to 0 *)
 
 Theorem neq_O_lt : forall n, 0 <> n -> 0 < n.
 Proof.
-induction n; auto with arith.
-intros; absurd (0 = 0); trivial with arith.
+  induction n; auto with arith.
+  intros; absurd (0 = 0); trivial with arith.
 Qed.
 Hint Immediate neq_O_lt: arith v62.
 
 Theorem lt_O_neq : forall n, 0 < n -> 0 <> n.
 Proof.
-induction 1; auto with arith.
+  induction 1; auto with arith.
 Qed.
 Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 7f5c1148..e0222e41 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Max.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Arith.
 
@@ -14,66 +14,66 @@ Open Local Scope nat_scope.
 
 Implicit Types m n : nat.
 
-(** maximum of two natural numbers *)
+(** * 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')
+    | O, _ => m
+    | S n', O => n
+    | S n', S m' => S (max n' m')
   end.
 
-(** Simplifications of [max] *)
+(** * Simplifications of [max] *)
 
 Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 
 Lemma max_comm : forall n m, max n m = max m n.
 Proof.
-induction n; induction m; simpl in |- *; auto with arith.
+  induction n; induction m; simpl in |- *; auto with arith.
 Qed.
 
-(** [max] and [le] *)
+(** * [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.
+  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.
+  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.
+  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.
+  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] *)
+(** * [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.
+  induction n; induction m; simpl in |- *; auto with arith.
+  elim (IHn m); intro H; elim H; auto.
 Qed.
 
 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.
+  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.
 Qed.
 
 Notation max_case2 := max_case (only parsing).
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 38351817..db14e74b 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -6,73 +6,73 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Min.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Min.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
-Require Import Arith.
+Require Import Le.
 
 Open Local Scope nat_scope.
 
 Implicit Types m n : nat.
 
-(** minimum of two natural numbers *)
+(** * 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')
+    | O, _ => 0
+    | S n', O => 0
+    | S n', S m' => S (min n' m')
   end.
 
-(** Simplifications of [min] *)
+(** * Simplifications of [min] *)
 
 Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 
 Lemma min_comm : forall n m, min n m = min m n.
 Proof.
-induction n; induction m; simpl in |- *; auto with arith.
+  induction n; induction m; simpl in |- *; auto with arith.
 Qed.
 
-(** [min] and [le] *)
+(** * [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.
+  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.
+  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.
+  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.
+  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] *)
+(** * [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.
+  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.
+  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.
 
 Notation min_case2 := min_case (only parsing).
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index dfecd7cf..2380c2de 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,9 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Minus.v 8642 2006-03-17 10:09:02Z notin $ i*)
-
-(** Subtraction (difference between two natural numbers) *)
+(*i $Id: Minus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+
+(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
+<<
+Fixpoint minus (n m:nat) {struct n} : nat :=
+  match n, m with
+  | O, _ => 0
+  | S k, O => S k
+  | S k, S l => k - l
+  end
+where "n - m" := (minus n m) : nat_scope.
+>>
+*)
 
 Require Import Lt.
 Require Import Le.
@@ -17,36 +27,37 @@ Open Local Scope nat_scope.
 
 Implicit Types m n p : nat.
 
-(** 0 is right neutral *)
+(** * 0 is right neutral *)
 
 Lemma minus_n_O : forall n, n = n - 0.
 Proof.
-induction n; simpl in |- *; auto with arith.
+  induction n; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve minus_n_O: arith v62.
 
-(** Permutation with successor *)
+(** * Permutation with successor *)
 
 Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
 Proof.
-intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
- auto with arith.
+  intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
+    auto with arith.
 Qed.
 Hint Resolve minus_Sn_m: arith v62.
 
 Theorem pred_of_minus : forall n, pred n = n - 1.
-intro x; induction x; simpl in |- *; auto with arith.
+Proof.
+  intro x; induction x; simpl in |- *; auto with arith.
 Qed.
 
-(** Diagonal *)
+(** * Diagonal *)
 
 Lemma minus_n_n : forall n, 0 = n - n.
 Proof.
-induction n; simpl in |- *; auto with arith.
+  induction n; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve minus_n_n: arith v62.
 
-(** Simplification *)
+(** * Simplification *)
 
 Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
 Proof.
@@ -54,70 +65,71 @@ Proof.
 Qed.
 Hint Resolve minus_plus_simpl_l_reverse: arith v62.
 
-(** Relation with plus *)
+(** * Relation with plus *)
 
 Lemma plus_minus : forall n m p, n = m + p -> p = n - m.
 Proof.
-intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *;
- intros.
-replace (n0 - 0) with n0; auto with arith.
-absurd (0 = S (n0 + p)); auto with arith.
-auto with arith.
+  intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *;
+    intros.
+  replace (n0 - 0) with n0; auto with arith.
+  absurd (0 = S (n0 + p)); auto with arith.
+  auto with arith.
 Qed.
 Hint Immediate plus_minus: arith v62.
 
 Lemma minus_plus : forall n m, n + m - n = m.
-symmetry  in |- *; auto with arith.
+  symmetry  in |- *; auto with arith.
 Qed.
 Hint Resolve minus_plus: arith v62.
 
 Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n).
 Proof.
-intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *;
- auto with arith.
+  intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *;
+    auto with arith.
 Qed.
 Hint Resolve le_plus_minus: arith v62.
 
 Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m.
 Proof.
-symmetry  in |- *; auto with arith.
+  symmetry  in |- *; auto with arith.
 Qed.
 Hint Resolve le_plus_minus_r: arith v62.
 
-(** Relation with order *)
+(** * Relation with order *)
 
 Theorem le_minus : forall n m, n - m <= n.
 Proof.
-intros i h; pattern i, h in |- *; apply nat_double_ind;
- [ auto
- | auto
- | intros m n H; simpl in |- *; apply le_trans with (m := m); auto ].
+  intros i h; pattern i, h in |- *; apply nat_double_ind;
+    [ auto
+      | auto
+      | intros m n H; simpl in |- *; apply le_trans with (m := m); auto ].
 Qed.
 
 Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
 Proof.
-intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
- auto with arith.
-intros; absurd (0 < 0); auto with arith.
-intros p q lepq Hp gtp.
-elim (le_lt_or_eq 0 p); auto with arith.
-auto with arith.
-induction 1; elim minus_n_O; auto with arith.
+  intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
+    auto with arith.
+  intros; absurd (0 < 0); auto with arith.
+  intros p q lepq Hp gtp.
+  elim (le_lt_or_eq 0 p); auto with arith.
+  auto with arith.
+  induction 1; elim minus_n_O; auto with arith.
 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 in |- *; apply nat_double_ind; simpl in |- *;
- auto with arith.
-intros; absurd (0 < 0); trivial with arith.
+  intros n m; pattern n, m in |- *; apply nat_double_ind; simpl in |- *;
+    auto with arith.
+  intros; absurd (0 < 0); trivial with arith.
 Qed.
 Hint Immediate lt_O_minus_lt: arith v62.
 
 Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0.
-intros y x; pattern y, x in |- *; apply nat_double_ind;
- [ simpl in |- *; trivial with arith
- | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ]
- | simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3;
-    apply H2; apply le_n_S; assumption ].
-Qed.
\ No newline at end of file
+Proof.
+  intros y x; pattern y, x in |- *; apply nat_double_ind;
+    [ simpl in |- *; trivial with arith
+      | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ]
+      | simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3;
+	apply H2; apply le_n_S; assumption ].
+Qed.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 051f8645..2315e12c 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 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Mult.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Export Plus.
 Require Export Minus.
@@ -17,86 +17,98 @@ Open Local Scope nat_scope.
 
 Implicit Types m n p : nat.
 
-(** Zero property *)
+(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *)
+
+(** * [nat] is a semi-ring *)
+
+(** ** Zero property *)
 
 Lemma mult_0_r : forall n, n * 0 = 0.
 Proof.
-intro; symmetry  in |- *; apply mult_n_O.
+  intro; symmetry  in |- *; apply mult_n_O.
 Qed.
 
 Lemma mult_0_l : forall n, 0 * n = 0.
 Proof.
-reflexivity.
+  reflexivity.
 Qed.
 
-(** Distributivity *)
+(** ** 1 is neutral *)
 
-Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
+Lemma mult_1_l : forall n, 1 * n = n.
 Proof.
-intros; elim n; simpl in |- *; intros; auto with arith.
-elim plus_assoc; elim H; auto with arith.
+  simpl in |- *; auto with arith.
 Qed.
-Hint Resolve mult_plus_distr_r: arith v62.
+Hint Resolve mult_1_l: arith v62.
 
-Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
+Lemma mult_1_r : forall n, n * 1 = n.
 Proof.
-  induction n. trivial.
-  intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4.
+  induction n; [ trivial | 
+    simpl; rewrite IHn; reflexivity].
 Qed.
+Hint Resolve mult_1_r: arith v62.
 
-Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
+(** ** Commutativity *)
+
+Lemma mult_comm : forall n m, n * m = m * n.
 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; elim n; intros; simpl in |- *; auto with arith.
+elim mult_n_Sm.
+elim H; apply plus_comm.
 Qed.
-Hint Resolve mult_minus_distr_r: arith v62.
+Hint Resolve mult_comm: arith v62.
 
-(** Associativity *)
+(** ** Distributivity *)
 
-Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
+Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
 Proof.
-intros; elim n; intros; simpl in |- *; auto with arith.
-rewrite mult_plus_distr_r.
-elim H; auto with arith.
+  intros; elim n; simpl in |- *; intros; auto with arith.
+  elim plus_assoc; elim H; auto with arith.
 Qed.
-Hint Resolve mult_assoc_reverse: arith v62.
+Hint Resolve mult_plus_distr_r: arith v62.
 
-Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
+Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
 Proof.
-auto with arith.
+  induction n. trivial.
+  intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4.
 Qed.
-Hint Resolve mult_assoc: arith v62.
 
-(** Commutativity *)
+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.
+Qed.
+Hint Resolve mult_minus_distr_r: arith v62.
 
-Lemma mult_comm : forall n m, n * m = m * n.
+Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p.
 Proof.
-intros; elim n; intros; simpl in |- *; auto with arith.
-elim mult_n_Sm.
-elim H; apply plus_comm.
+  intros n m p. rewrite mult_comm. rewrite mult_minus_distr_r. 
+  rewrite (mult_comm m n); rewrite (mult_comm p n); reflexivity.
 Qed.
-Hint Resolve mult_comm: arith v62.
+Hint Resolve mult_minus_distr_l: arith v62.
 
-(** 1 is neutral *)
+(** ** Associativity *)
 
-Lemma mult_1_l : forall n, 1 * n = n.
+Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
 Proof.
-simpl in |- *; auto with arith.
+  intros; elim n; intros; simpl in |- *; auto with arith.
+  rewrite mult_plus_distr_r.
+  elim H; auto with arith.
 Qed.
-Hint Resolve mult_1_l: arith v62.
+Hint Resolve mult_assoc_reverse: arith v62.
 
-Lemma mult_1_r : forall n, n * 1 = n.
+Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
 Proof.
-intro; elim mult_comm; auto with arith.
+  auto with arith.
 Qed.
-Hint Resolve mult_1_r: arith v62.
+Hint Resolve mult_assoc: arith v62.
 
-(** Compatibility with orders *)
+(** * Compatibility with orders *)
 
 Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
 Proof.
-induction m; simpl in |- *; auto with arith.
+  induction m; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve mult_O_le: arith v62.
 
@@ -110,26 +122,27 @@ Hint Resolve mult_le_compat_l: arith.
 
 
 Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
-intros m n p H.
-rewrite mult_comm. rewrite (mult_comm n).
-auto with arith.
+Proof.
+  intros m n p H.
+  rewrite mult_comm. rewrite (mult_comm n).
+  auto with arith.
 Qed.
 
 Lemma mult_le_compat :
- forall n m p (q:nat), 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 in |- *; apply le_trans with (m0 * q).
-assumption.
-apply le_plus_r.
+  forall n m p (q:nat), 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 in |- *; apply le_trans with (m0 * q).
+  assumption.
+  apply le_plus_r.
 Qed.
 
 Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
@@ -141,11 +154,12 @@ Qed.
 Hint Resolve mult_S_lt_compat_l: arith.
 
 Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
-intros m n p H H0.
-induction p.
-elim (lt_irrefl _ H0).
-rewrite mult_comm.
-replace (n * S p) with (S p * n); auto with arith.
+Proof.
+  intros m n p H H0.
+  induction p.
+  elim (lt_irrefl _ H0).
+  rewrite mult_comm.
+  replace (n * S p) with (S p * n); auto with arith.
 Qed.
 
 Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
@@ -156,27 +170,28 @@ Proof.
   apply mult_S_lt_compat_l. assumption.
 Qed.
 
-(** n|->2*n and n|->2n+1 have disjoint image *)
+(** * n|->2*n and n|->2n+1 have disjoint image *)
 
 Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.
-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.
+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.
 Qed.
 
 
-(** Tail-recursive mult *)
+(** * Tail-recursive mult *)
 
 (** [tail_mult] is an alternative definition for [mult] which is 
     tail-recursive, whereas [mult] is not. This can be useful 
@@ -184,23 +199,23 @@ Qed.
 
 Fixpoint mult_acc (s:nat) m n {struct n} : nat :=
   match n with
-  | O => s
-  | S p => mult_acc (tail_plus m s) m p
+    | O => s
+    | S p => mult_acc (tail_plus m s) m p
   end.
 
 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_comm; auto.
+  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_comm; auto.
 Qed.
 
 Definition tail_mult n m := mult_acc 0 m n.
 
 Lemma mult_tail_mult : forall n m, n * m = tail_mult n m.
 Proof.
-intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
+  intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
 Qed.
 
 (** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] 
@@ -208,4 +223,4 @@ Qed.
 
 Ltac tail_simpl :=
   repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
-   simpl in |- *. 
\ No newline at end of file
+    simpl in |- *.
\ No newline at end of file
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 4aef7dc0..b17021bc 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 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Peano_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Decidable.
 
@@ -16,19 +16,19 @@ Implicit Types m n x y : nat.
 
 Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}.
 Proof.
-induction n.
-auto.
-left; exists n; auto.
+  induction n.
+  auto.
+  left; exists n; auto.
 Defined.
 
 Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
 Proof.
-induction n; induction m; auto.
-elim (IHn m); auto.
+  induction n; induction m; auto.
+  elim (IHn m); auto.
 Defined.
 
 Hint Resolve O_or_S eq_nat_dec: arith.
 
 Theorem dec_eq_nat : forall n m, decidable (n = m).
-intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith.
+  intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith.
 Defined.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 56e1c58a..74d0dc93 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,9 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Plus.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Plus.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
-(** Properties of addition *)
+(** Properties of addition. [add] is defined in [Init/Peano.v] as:
+<<
+Fixpoint plus (n m:nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (p + m)
+  end
+where "n + m" := (plus n m) : nat_scope.
+>>
+ *)
 
 Require Import Le.
 Require Import Lt.
@@ -17,126 +26,127 @@ Open Local Scope nat_scope.
 
 Implicit Types m n p q : nat.
 
-(** Zero is neutral *)
+(** * Zero is neutral *)
 
 Lemma plus_0_l : forall n, 0 + n = n.
 Proof.
-reflexivity.
+  reflexivity.
 Qed.
 
 Lemma plus_0_r : forall n, n + 0 = n.
 Proof.
-intro; symmetry  in |- *; apply plus_n_O.
+  intro; symmetry  in |- *; apply plus_n_O.
 Qed.
 
-(** Commutativity *)
+(** * Commutativity *)
 
 Lemma plus_comm : forall n m, n + m = m + n.
 Proof.
-intros n m; elim n; simpl in |- *; auto with arith.
-intros y H; elim (plus_n_Sm m y); auto with arith.
+  intros n m; elim n; simpl in |- *; auto with arith.
+  intros y H; elim (plus_n_Sm m y); auto with arith.
 Qed.
 Hint Immediate plus_comm: arith v62.
 
-(** Associativity *)
+(** * Associativity *)
 
 Lemma plus_Snm_nSm : forall n m, S n + m = n + S m.
-intros.
-simpl in |- *.
-rewrite (plus_comm n m).
-rewrite (plus_comm n (S m)).
-trivial with arith.
+Proof.
+  intros.
+  simpl in |- *.
+  rewrite (plus_comm n m).
+  rewrite (plus_comm n (S m)).
+  trivial with arith.
 Qed.
 
 Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
 Proof.
-intros n m p; elim n; simpl in |- *; auto with arith.
+  intros n m p; elim n; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve plus_assoc: arith v62.
 
 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.
+  intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith.
 Qed.
 
 Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p).
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 Hint Resolve plus_assoc_reverse: arith v62.
 
-(** Simplification *)
+(** * Simplification *)
 
 Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.
 Proof.
-intros m p n; induction n; simpl in |- *; auto with arith.
+  intros m p n; induction n; simpl in |- *; auto with arith.
 Qed.
 
 Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
 Proof.
-induction p; simpl in |- *; auto with arith.
+  induction p; simpl in |- *; auto with arith.
 Qed.
 
 Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
 Proof.
-induction p; simpl in |- *; auto with arith.
+  induction p; simpl in |- *; auto with arith.
 Qed.
 
-(** Compatibility with order *)
+(** * Compatibility with order *)
 
 Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.
 Proof.
-induction p; simpl in |- *; auto with arith.
+  induction p; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve plus_le_compat_l: arith v62.
 
 Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p.
 Proof.
-induction 1; simpl in |- *; auto with arith.
+  induction 1; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve plus_le_compat_r: arith v62.
 
 Lemma le_plus_l : forall n m, n <= n + m.
 Proof.
-induction n; simpl in |- *; auto with arith.
+  induction n; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve le_plus_l: arith v62.
 
 Lemma le_plus_r : forall n m, m <= n + m.
 Proof.
-intros n m; elim n; simpl in |- *; auto with arith.
+  intros n m; elim n; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve le_plus_r: arith v62.
 
 Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p.
 Proof.
-intros; apply le_trans with (m := m); auto with arith.
+  intros; apply le_trans with (m := m); auto with arith.
 Qed.
 Hint Resolve le_plus_trans: arith v62.
 
 Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
 Proof.
-intros; apply lt_le_trans with (m := m); auto with arith.
+  intros; apply lt_le_trans with (m := m); auto with arith.
 Qed.
 Hint Immediate lt_plus_trans: arith v62.
 
 Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
 Proof.
-induction p; simpl in |- *; auto with arith.
+  induction p; simpl in |- *; auto with arith.
 Qed.
 Hint Resolve plus_lt_compat_l: arith v62.
 
 Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
 Proof.
-intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p).
-elim p; auto with arith.
+  intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p).
+  elim p; auto with arith.
 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.
 Proof.
-intros n m p q H H0.
-elim H; simpl in |- *; auto with arith.
+  intros n m p q H H0.
+  elim H; simpl in |- *; auto with arith.
 Qed.
 
 Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
@@ -156,7 +166,7 @@ Proof.
   apply lt_le_weak. assumption.
 Qed.
 
-(** Inversion lemmas *)
+(** * Inversion lemmas *)
 
 Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0.
 Proof.
@@ -173,7 +183,7 @@ Proof.
   simpl in H. discriminate H.
 Defined.
 
-(** Derived properties *)
+(** * Derived properties *)
 
 Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).
 Proof.
@@ -182,7 +192,7 @@ Proof.
   rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc.
 Qed.
 
-(** Tail-recursive plus *)
+(** * Tail-recursive plus *)
 
 (** [tail_plus] is an alternative definition for [plus] which is 
     tail-recursive, whereas [plus] is not. This can be useful
@@ -190,8 +200,8 @@ Qed.
 
 Fixpoint plus_acc q n {struct n} : nat :=
   match n with
-  | O => q
-  | S p => plus_acc (S q) p
+    | O => q
+    | S p => plus_acc (S q) p
   end.
 
 Definition tail_plus n m := plus_acc m n.
@@ -201,27 +211,27 @@ unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto.
 intro m; rewrite <- IHn; simpl in |- *; auto.
 Qed.
 
-(** Discrimination *)
+(** * Discrimination *)
 
 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; 
-   reflexivity.
+  intros n m; induction n as [|n IHn].
+  discriminate.
+  intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; 
+    reflexivity.
 Qed.
 
 Lemma n_SSn : forall n, n <> S (S n).
 Proof.
-intro n; exact (succ_plus_discr n 1).
+  intro n; exact (succ_plus_discr n 1).
 Qed.
 
 Lemma n_SSSn : forall n, n <> S (S (S n)).
 Proof.
-intro n; exact (succ_plus_discr n 2).
+  intro n; exact (succ_plus_discr n 2).
 Qed.
 
 Lemma n_SSSSn : forall n, n <> S (S (S (S n))).
 Proof.
-intro n; exact (succ_plus_discr n 3).
+  intro n; exact (succ_plus_discr n 3).
 Qed.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index e1bbfad9..11fcd161 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 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Wf_nat.v 9341 2006-11-06 13:08:10Z notin $ i*)
 
 (** Well-founded relations and natural numbers *)
 
@@ -18,7 +18,7 @@ Implicit Types m n p : nat.
 
 Section Well_founded_Nat.
 
-Variable A : Set.
+Variable A : Type.
 
 Variable f : A -> nat.
 Definition ltof (a b:A) := f a < f b.
@@ -26,21 +26,21 @@ Definition gtof (a b:A) := f b > f a.
 
 Theorem well_founded_ltof : well_founded ltof.
 Proof.
-red in |- *.
-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 in |- *; intros b ltfafb.
-apply IHn.
-apply lt_le_trans with (f a); auto with arith.
+  red in |- *.
+  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 in |- *; intros b ltfafb.
+  apply IHn.
+  apply lt_le_trans with (f a); auto with arith.
 Defined.
 
 Theorem well_founded_gtof : well_founded gtof.
 Proof.
-exact well_founded_ltof.
+  exact well_founded_ltof.
 Defined.
 
 (** It is possible to directly prove the induction principle going
@@ -48,52 +48,55 @@ Defined.
    or to use the previous lemmas to extract a program with a fixpoint
    ([induction_ltof2]) 
 
-the ML-like program for [induction_ltof1] is : [[
+the ML-like program for [induction_ltof1] is : 
+[[
    let induction_ltof1 F a = indrec ((f a)+1) a 
    where rec indrec = 
         function 0    -> (function a -> error)
                |(S m) -> (function a -> (F a (function y -> indrec y m)));;
 ]]
 
-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;;
-]] *)
+]]
+*)
 
 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 in |- *; intros b ltfafb.
-apply IHn.
-apply lt_le_trans with (f a); auto with arith.
+  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 in |- *; intros b ltfafb.
+  apply IHn.
+  apply lt_le_trans with (f a); auto with arith.
 Defined. 
 
 Theorem induction_gtof1 :
- forall P:A -> Set,
-   (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
+  forall P:A -> Set,
+    (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
-exact induction_ltof1.
+  exact induction_ltof1.
 Defined.
 
 Theorem induction_ltof2 :
- forall P:A -> Set,
-   (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
+  forall P:A -> Set,
+    (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
-exact (well_founded_induction well_founded_ltof).
+  exact (well_founded_induction well_founded_ltof).
 Defined.
 
 Theorem induction_gtof2 :
- forall P:A -> Set,
-   (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
+  forall P:A -> Set,
+    (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
-exact induction_ltof2.
+  exact induction_ltof2.
 Defined.
 
 (** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
@@ -105,105 +108,105 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
 
 Theorem well_founded_lt_compat : well_founded R.
 Proof.
-red in |- *.
-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.
+  red in |- *.
+  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.
 Defined.
 
 End Well_founded_Nat.
 
 Lemma lt_wf : well_founded lt.
 Proof.
-exact (well_founded_ltof nat (fun m => m)).
+  exact (well_founded_ltof nat (fun m => m)).
 Defined.
 
 Lemma lt_wf_rec1 :
- forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+  forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
 Proof.
-exact (fun p P F => induction_ltof1 nat (fun m => m) P F p).
+  exact (fun p P F => induction_ltof1 nat (fun m => m) P F p).
 Defined.
 
 Lemma lt_wf_rec :
- forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+  forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
 Proof.
-exact (fun p P F => induction_ltof2 nat (fun m => m) P F p).
+  exact (fun p P F => induction_ltof2 nat (fun m => m) P F p).
 Defined.
 
 Lemma lt_wf_ind :
- forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+  forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
 Proof.
-intro p; intros; elim (lt_wf p); auto with arith.
+  intro p; intros; elim (lt_wf p); auto with arith.
 Qed.
 
 Lemma gt_wf_rec :
- forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
+  forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
 Proof.
-exact lt_wf_rec.
+  exact lt_wf_rec.
 Defined.
 
 Lemma gt_wf_ind :
- forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
+  forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
 Proof lt_wf_ind.
 
 Lemma lt_wf_double_rec :
  forall P:nat -> nat -> Set,
    (forall n m,
-      (forall p q, p < n -> P p q) ->
-      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
+     (forall p q, p < n -> P p q) ->
+     (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
 Proof.
-intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
-intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
+  intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
+  intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
 Defined.
 
 Lemma lt_wf_double_ind :
- forall P:nat -> nat -> Prop,
-   (forall n m,
+  forall P:nat -> nat -> Prop,
+    (forall n m,
       (forall p (q:nat), p < n -> P p q) ->
       (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
 Proof.
-intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
-intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
+  intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
+  intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
 Qed.
 
 Hint Resolve lt_wf: arith.
 Hint Resolve well_founded_lt_compat: arith.
 
 Section LT_WF_REL.
-Variable A : Set.
-Variable R : A -> A -> Prop.
-
-(* Relational form of inversion *)
-Variable F : A -> nat -> Prop.
-Definition inv_lt_rel x y := exists2 n, F x n & (forall m, F y m -> n < m).
-
-Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
-Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
-Proof.
-intros x [n fxn]; generalize dependent x.
-pattern n in |- *; apply lt_wf_ind; intros.
-constructor; intros.
-destruct (F_compat y x) as (x0,H1,H2); trivial.
-apply (H x0); auto.
-Qed.
-
-Theorem well_founded_inv_lt_rel_compat : well_founded R.
-Proof.
-constructor; intros.
-case (F_compat y a); trivial; intros.
-apply acc_lt_rel; trivial.
-exists x; trivial.
-Qed.
+  Variable A : Set.
+  Variable R : A -> A -> Prop.
+
+  (* Relational form of inversion *)
+  Variable F : A -> nat -> Prop.
+  Definition inv_lt_rel x y := exists2 n, F x n & (forall m, F y m -> n < m).
+
+  Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
+  Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
+  Proof.
+    intros x [n fxn]; generalize dependent x.
+    pattern n in |- *; apply lt_wf_ind; intros.
+    constructor; intros.
+    destruct (F_compat y x) as (x0,H1,H2); trivial.
+    apply (H x0); auto.
+  Qed.
+
+  Theorem well_founded_inv_lt_rel_compat : well_founded R.
+  Proof.
+    constructor; intros.
+    case (F_compat y a); trivial; intros.
+    apply acc_lt_rel; trivial.
+    exists x; trivial.
+  Qed.
 
 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).
-intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
+  forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
+  intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
 Qed.