Imported Upstream version 8.0pl1upstream/8.0pl1

22 files changed, 2598 insertions, 0 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
new file mode 100755
index 00000000..d44efb56
--- /dev/null
+++ b/theories/Arith/Arith.v
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  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: Arith.v,v 1.11.2.1 2004/07/16 19:30:59 herbelin Exp $ i*)
+
+Require Export Le.
+Require Export Lt.
+Require Export Plus.
+Require Export Gt.
+Require Export Minus.
+Require Export Mult.
+Require Export Between.
+Require Export Minus.
+Require Export Peano_dec.
+Require Export Compare_dec.
+Require Export Factorial.
\ No newline at end of file
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
new file mode 100755
index 00000000..448ce002
--- /dev/null
+++ b/theories/Arith/Between.v
@@ -0,0 +1,189 @@
+(************************************************************************)
+(*  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: Between.v,v 1.12.2.1 2004/07/16 19:30:59 herbelin Exp $ i*)
+
+Require Import Le.
+Require Import Lt.
+
+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 :
+      forall k l (n:nat),
+        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.
+
+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.
+
+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
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
new file mode 100644
index 00000000..55dfd47f
--- /dev/null
+++ b/theories/Arith/Bool_nat.v
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: Bool_nat.v,v 1.5.2.1 2004/07/16 19:30:59 herbelin Exp $ *)
+
+Require Export Compare_dec.
+Require Export Peano_dec.
+Require Import Sumbool.
+
+Open Local Scope nat_scope.
+
+Implicit Types m n x y : nat.
+
+(** The decidability of equality and order relations over
+    type [nat] give some boolean functions with the adequate specification. *)
+
+Definition notzerop n := sumbool_not _ _ (zerop n).
+Definition lt_ge_dec : forall x y, {x < y} + {x >= y} :=
+  fun n m => sumbool_not _ _ (le_lt_dec m n).
+
+Definition nat_lt_ge_bool x y := bool_of_sumbool (lt_ge_dec x y).
+Definition nat_ge_lt_bool x y :=
+  bool_of_sumbool (sumbool_not _ _ (lt_ge_dec x y)).
+
+Definition nat_le_gt_bool x y := bool_of_sumbool (le_gt_dec x y).
+Definition nat_gt_le_bool x y :=
+  bool_of_sumbool (sumbool_not _ _ (le_gt_dec x y)).
+
+Definition nat_eq_bool x y := bool_of_sumbool (eq_nat_dec x y).
+Definition nat_noteq_bool x y :=
+  bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)).
+
+Definition zerop_bool x := bool_of_sumbool (zerop x).
+Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
new file mode 100755
index 00000000..46827bae
--- /dev/null
+++ b/theories/Arith/Compare.v
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*  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: Compare.v,v 1.12.2.1 2004/07/16 19:31:00 herbelin Exp $ 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 Peano_dec.
+Require Import Compare_dec.
+
+Definition le_or_le_S := le_le_S_dec.
+
+Definition Pcompare := gt_eq_gt_dec.
+
+Lemma le_dec : forall n m, {n <= m} + {m <= n}.
+Proof le_ge_dec.
+
+Definition lt_or_eq n m := {m > n} + {n = m}.
+
+Lemma le_decide : forall n m, n <= m -> lt_or_eq n m.
+Proof le_lt_eq_dec.
+
+Lemma le_le_S_eq : forall n m, n <= m -> S n <= m \/ n = m.
+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))).
+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.
+Qed.
+
+Require Export Wf_nat.
+
+Require Export Min.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
new file mode 100755
index 00000000..ea21437d
--- /dev/null
+++ b/theories/Arith/Compare_dec.v
@@ -0,0 +1,107 @@
+(************************************************************************)
+(*  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: Compare_dec.v,v 1.13.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Le.
+Require Import Lt.
+Require Import Gt.
+Require Import Decidable.
+
+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.
+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.
+Defined.
+
+Lemma gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}.
+Proof lt_eq_lt_dec.
+
+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.
+Defined.
+
+Definition le_le_S_dec : forall n m, {n <= m} + {S m <= n}.
+Proof.
+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.
+Defined.
+
+Definition le_gt_dec : forall n m, {n <= m} + {n > m}.
+Proof.
+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.
+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 ].
+Qed.
+
+Theorem dec_lt : forall n m, decidable (n < m).
+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.
+Qed.
+
+Theorem dec_ge : forall n m, decidable (n >= m).
+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 ].
+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 ].
+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 ].
+Qed.
+
+Theorem not_ge : forall n m, ~ n >= m -> n < m.
+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). 
+Qed.
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
new file mode 100755
index 00000000..adb5593d
--- /dev/null
+++ b/theories/Arith/Div.v
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Div.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+(** Euclidean division *)
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
+
+Require Le.
+Require Euclid_def.
+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.
+
+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.
+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.
+Qed.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
new file mode 100644
index 00000000..c005f061
--- /dev/null
+++ b/theories/Arith/Div2.v
@@ -0,0 +1,175 @@
+(************************************************************************)
+(*  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: Div2.v,v 1.15.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Lt.
+Require Import Plus.
+Require Import Compare_dec.
+Require Import Even.
+
+Open Local Scope nat_scope.
+
+Implicit Type n : nat.
+
+(** Here we define [n/2] and prove some of its properties *)
+
+Fixpoint div2 n : nat :=
+  match n with
+  | O => 0
+  | S O => 0
+  | S (S n') => S (div2 n')
+  end.
+
+(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
+    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.
+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.
+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.
+Qed.
+
+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)).
+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.
+Qed.
+
+(** Specializations *)
+
+Lemma even_div2 : forall n, even n -> div2 n = div2 (S n).
+Proof fun n => proj1 (proj1 (even_odd_div2 n)).
+
+Lemma div2_even : forall n, div2 n = div2 (S n) -> even n.
+Proof fun n => proj2 (proj1 (even_odd_div2 n)).
+
+Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
+Proof fun n => proj1 (proj2 (even_odd_div2 n)).
+
+Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Proof fun n => proj2 (proj2 (even_odd_div2 n)).
+
+Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
+
+(** Properties related to the double ([2n]) *)
+
+Definition double n := n + n.
+
+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.
+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.
+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))).
+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.
+Qed.
+
+
+(** Specializations *)
+
+Lemma even_double : forall n, even n -> n = double (div2 n).
+Proof fun n => proj1 (proj1 (even_odd_double n)).
+
+Lemma double_even : forall n, n = double (div2 n) -> even n.
+Proof fun n => proj2 (proj1 (even_odd_double n)).
+
+Lemma odd_double : forall n, odd n -> n = S (double (div2 n)).
+Proof fun n => proj1 (proj2 (even_odd_double n)).
+
+Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n.
+Proof fun n => proj2 (proj2 (even_odd_double n)).
+
+Hint Resolve even_double double_even odd_double double_odd: arith.
+
+(** Application: 
+    - if [n] is even then there is a [p] such that [n = 2p]
+    - if [n] is odd  then there is a [p] such that [n = 2p+1]
+
+    (Immediate: it is [n/2]) *)
+
+Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
+Proof.
+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.
+Qed.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
new file mode 100755
index 00000000..2e99e068
--- /dev/null
+++ b/theories/Arith/EqNat.v
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  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: EqNat.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+(** Equality on natural numbers *)
+
+Open Local Scope nat_scope.
+
+Implicit Types m n x y : nat.
+
+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
+  end.
+
+Theorem eq_nat_refl : forall n, eq_nat n n.
+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.
+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.
+Qed.
+Hint Immediate eq_nat_eq: arith v62.
+
+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.
+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.
+Defined.
+
+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
+  end.
+
+Lemma beq_nat_refl : forall n, true = beq_nat n n.
+Proof.
+  intro x; induction x; simpl in |- *; auto.
+Qed.
+
+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.
+Defined.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
new file mode 100644
index 00000000..e50e3d70
--- /dev/null
+++ b/theories/Arith/Euclid.v
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*  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: Euclid.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Mult.
+Require Import Compare_dec.
+Require Import Wf_nat.
+
+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.
+
+
+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.
+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.
+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
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
new file mode 100644
index 00000000..f7a2ad71
--- /dev/null
+++ b/theories/Arith/Even.v
@@ -0,0 +1,305 @@
+(************************************************************************)
+(*  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: Even.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+(** Here we define the predicates [even] and [odd] by mutual induction
+    and we prove the decidability and the exclusion of those predicates.
+    The main results about parity are proved in the module Div2. *)
+
+Open Local Scope nat_scope.
+
+Implicit Types m n : nat.
+
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+    odd_S : forall n, even n -> odd (S n).
+
+Hint Constructors even: arith.
+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.
+Qed.
+
+Lemma even_odd_dec : forall n, {even n} + {odd n}.
+Proof.
+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.
+Qed.
+
+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).
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+Qed.
+Hint Resolve odd_plus_l odd_plus_r: arith.
+ 
+Lemma even_mult_aux :
+ forall n m,
+   (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
+Proof.
+intros n; elim n; simpl 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.
+Qed.
+ 
+Lemma even_mult_r : forall n m, even m -> even (n * m).
+Proof.
+intros n m; case (even_mult_aux n m); auto.
+intros H H0; case H0; auto.
+Qed.
+Hint Resolve even_mult_l even_mult_r: arith.
+ 
+Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m.
+Proof.
+intros n m H' H'0.
+case (even_mult_aux n m).
+intros H'1 H'2; elim H'2.
+intros H'3; elim H'3; auto.
+intros H; case (not_even_and_odd n); auto.
+Qed.
+ 
+Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.
+Proof.
+intros n m H' H'0.
+case (even_mult_aux n m).
+intros H'1 H'2; elim H'2.
+intros H'3; elim H'3; auto.
+intros H; case (not_even_and_odd m); auto.
+Qed.
+ 
+Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m).
+Proof.
+intros n m; case (even_mult_aux n m); intros H; case H; auto.
+Qed.
+Hint Resolve even_mult_l even_mult_r odd_mult: arith.
+ 
+Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n.
+Proof.
+intros n m H'.
+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.
+Qed.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
new file mode 100644
index 00000000..4db211e4
--- /dev/null
+++ b/theories/Arith/Factorial.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  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: Factorial.v,v 1.5.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Plus.
+Require Import Mult.
+Require Import Lt.
+Open Local Scope nat_scope.
+
+(** Factorial *)
+
+Fixpoint fact (n:nat) : nat :=
+  match n with
+  | 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.
+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.
+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.
+Qed.
\ No newline at end of file
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
new file mode 100755
index 00000000..299c664d
--- /dev/null
+++ b/theories/Arith/Gt.v
@@ -0,0 +1,148 @@
+(************************************************************************)
+(*  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: Gt.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Le.
+Require Import Lt.
+Require Import Plus.
+Open Local Scope nat_scope.
+
+Implicit Types m n p : nat.
+
+(** Order and successor *)
+
+Theorem gt_Sn_O : forall n, S n > 0.
+Proof.
+  auto with arith.
+Qed.
+Hint Resolve gt_Sn_O: arith v62.
+
+Theorem gt_Sn_n : forall n, S n > n.
+Proof.
+  auto with arith.
+Qed.
+Hint Resolve gt_Sn_n: arith v62.
+
+Theorem gt_n_S : forall n m, n > m -> S n > S m.
+Proof.
+  auto with arith.
+Qed.
+Hint Resolve gt_n_S: arith v62.
+
+Lemma gt_S_n : forall n m, S m > S n -> m > n.
+Proof.
+  auto with arith.
+Qed.
+Hint Immediate gt_S_n: arith v62.
+
+Theorem gt_S : forall n m, S n > m -> n > m \/ m = n.
+Proof.
+  intros n m H; unfold gt in |- *; apply le_lt_or_eq; auto with arith.
+Qed.
+
+Lemma gt_pred : forall n m, m > S n -> pred m > n.
+Proof.
+  auto with arith.
+Qed.
+Hint Immediate gt_pred: arith v62.
+
+(** Irreflexivity *)
+
+Lemma gt_irrefl : forall n, ~ n > n.
+Proof lt_irrefl.
+Hint Resolve gt_irrefl: arith v62.
+
+(** 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 *)
+
+Lemma le_not_gt : forall n m, n <= m -> ~ n > m.
+Proof le_not_lt.
+Hint Resolve le_not_gt: arith v62.
+
+Lemma gt_not_le : forall n m, n > m -> ~ n <= m.
+Proof.
+auto with arith.
+Qed.
+
+Hint Resolve gt_not_le: arith v62.
+
+Theorem le_S_gt : forall n m, S n <= m -> m > n.
+Proof.
+  auto with arith.
+Qed.
+Hint Immediate le_S_gt: arith v62.
+
+Lemma gt_S_le : forall n m, S m > n -> n <= m.
+Proof.
+  intros n p; exact (lt_n_Sm_le n p).
+Qed.
+Hint Immediate gt_S_le: arith v62.
+
+Lemma gt_le_S : forall n m, m > n -> S n <= m.
+Proof.
+  auto with arith.
+Qed.
+Hint Resolve gt_le_S: arith v62.
+
+Lemma le_gt_S : forall n m, n <= m -> S m > n.
+Proof.
+  auto with arith.
+Qed.
+Hint Resolve le_gt_S: arith v62.
+
+(** Transitivity *)
+
+Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p.
+Proof.
+  red in |- *; intros; apply lt_le_trans with m; auto with arith.
+Qed.
+
+Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p.
+Proof.
+  red in |- *; intros; apply le_lt_trans with m; auto with arith.
+Qed.
+
+Lemma gt_trans : forall n m p, n > m -> m > p -> n > p.
+Proof.
+  red in |- *; intros n m p H1 H2.
+  apply lt_trans with m; auto with arith.
+Qed.
+
+Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p.
+Proof.
+  red in |- *; intros; apply lt_le_trans with m; auto with arith.
+Qed.
+
+Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
+
+(** Comparison to 0 *)
+
+Theorem gt_O_eq : forall n, n > 0 \/ 0 = n.
+Proof.
+  intro n; apply gt_S; auto with arith.
+Qed.
+
+(** Simplification and compatibility *)
+
+Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m.
+Proof.
+  red in |- *; intros n m p H; apply plus_lt_reg_l with p; auto with arith.
+Qed.
+
+Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
+Proof.
+  auto with arith.
+Qed.
+Hint Resolve plus_gt_compat_l: arith v62.
\ No newline at end of file
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
new file mode 100755
index 00000000..a5378cff
--- /dev/null
+++ b/theories/Arith/Le.v
@@ -0,0 +1,122 @@
+(************************************************************************)
+(*  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: Le.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+(** Order on natural numbers *)
+Open Local Scope nat_scope.
+
+Implicit Types m n p : nat.
+
+(** Reflexivity *)
+
+Theorem le_refl : forall n, n <= n.
+Proof.
+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 *)
+
+Theorem le_n_S : forall n m, n <= m -> S n <= S m.
+Proof.
+  induction 1; auto.
+Qed.
+
+Theorem le_n_Sn : forall n, n <= S n.
+Proof.
+  auto.
+Qed.
+
+Theorem le_O_n : forall n, 0 <= n.
+Proof.
+  induction n; auto.
+Qed.
+
+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.
+Proof.
+induction n; auto with arith.
+Qed.
+Hint Resolve le_pred_n: 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.
+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 |- *.
+elim H; simpl in |- *; auto with arith.
+Qed.
+Hint Immediate le_S_n: arith v62.
+
+Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
+Proof.
+induction n as [| n IHn]. simpl in |- *. auto with arith.
+destruct m as [| m]. simpl in |- *. intro H. inversion H.
+simpl in |- *. auto with arith.
+Qed.
+
+(** Comparison to 0 *)
+
+Theorem le_Sn_O : forall n, ~ S n <= 0.
+Proof.
+red in |- *; intros n H.
+change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve le_Sn_O: arith v62.
+
+Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n.
+Proof.
+induction n; auto with arith.
+intro; contradiction le_Sn_O with n.
+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.
+
+(** 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.
+Qed.
+Hint Immediate le_antisym: arith v62.
+
+(** A different elimination principle for the order on natural numbers *)
+
+Lemma le_elim_rel :
+ forall P:nat -> nat -> Prop,
+   (forall p, P 0 p) ->
+   (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
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
new file mode 100755
index 00000000..e1b3e4b8
--- /dev/null
+++ b/theories/Arith/Lt.v
@@ -0,0 +1,175 @@
+(************************************************************************)
+(*  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: Lt.v,v 1.11.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Le.
+Open Local Scope nat_scope.
+
+Implicit Types m n p : nat.
+
+(** Irreflexivity *)
+
+Theorem lt_irrefl : forall n, ~ n < n.
+Proof le_Sn_n.
+Hint Resolve lt_irrefl: arith v62.
+
+(** Relationship between [le] and [lt] *) 
+
+Theorem lt_le_S : forall n m, n < m -> S n <= m.
+Proof.
+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.
+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.
+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.
+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).
+Qed.
+Hint Immediate le_not_lt lt_not_le: arith v62.
+
+(** Asymmetry *)
+
+Theorem lt_asym : forall n m, n < m -> ~ m < n.
+Proof.
+induction 1; auto with arith.
+Qed.
+
+(** Order and successor *)
+
+Theorem lt_n_Sn : forall n, n < S n.
+Proof.
+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.
+Qed.
+Hint Resolve lt_S: arith v62.
+
+Theorem lt_n_S : forall n m, n < m -> S n < S m.
+Proof.
+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.
+Qed.
+Hint Immediate lt_S_n: arith v62.
+
+Theorem lt_O_Sn : forall n, 0 < S n.
+Proof.
+auto with arith.
+Qed.
+Hint Resolve lt_O_Sn: arith v62.
+
+Theorem lt_n_O : forall n, ~ n < 0.
+Proof le_Sn_O.
+Hint Resolve lt_n_O: arith v62.
+
+(** Predecessor *)
+
+Lemma S_pred : forall n m, m < n -> n = S (pred n).
+Proof.
+induction 1; auto with arith.
+Qed.
+
+Lemma lt_pred : forall n m, S n < m -> n < pred m.
+Proof.
+induction 1; simpl in |- *; auto with arith.
+Qed.
+Hint Immediate lt_pred: arith v62.
+
+Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n.
+destruct 1; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve lt_pred_n_n: arith v62.
+
+(** Transitivity properties *)
+
+Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
+Proof.
+induction 2; auto with arith.
+Qed.
+
+Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
+Proof.
+induction 2; auto with arith.
+Qed.
+
+Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
+Proof.
+induction 2; auto with arith.
+Qed.
+
+Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62.
+
+(** Large = strict or equal *)
+
+Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m.
+Proof.
+induction 1; auto with arith.
+Qed.
+
+Theorem lt_le_weak : forall n m, n < m -> n <= m.
+Proof.
+auto with arith.
+Qed.
+Hint Immediate lt_le_weak: arith v62.
+
+(** Dichotomy *)
+
+Theorem le_or_lt : forall n m, n <= m \/ m < n.
+Proof.
+intros n m; pattern n, m 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.
+Qed.
+
+(** 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.
+Qed.
+Hint Immediate neq_O_lt: arith v62.
+
+Theorem lt_O_neq : forall n, 0 < n -> 0 <> n.
+Proof.
+induction 1; auto with arith.
+Qed.
+Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
new file mode 100755
index 00000000..82673ed0
--- /dev/null
+++ b/theories/Arith/Max.v
@@ -0,0 +1,85 @@
+(************************************************************************)
+(*  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: Max.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Arith.
+
+Open Local Scope nat_scope.
+
+Implicit Types m n : nat.
+
+(** maximum of two natural numbers *)
+
+Fixpoint max n m {struct n} : nat :=
+  match n, m with
+  | O, _ => m
+  | S n', O => n
+  | S n', S m' => S (max n' m')
+  end.
+
+(** Simplifications of [max] *)
+
+Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
+Proof.
+auto with arith.
+Qed.
+
+Lemma max_comm : forall n m, max n m = max m n.
+Proof.
+induction n; induction m; simpl in |- *; auto with arith.
+Qed.
+
+(** [max] and [le] *)
+
+Lemma max_l : forall n m, m <= n -> max n m = n.
+Proof.
+induction n; induction m; simpl in |- *; auto with arith.
+Qed.
+
+Lemma max_r : forall n m, n <= m -> max n m = m.
+Proof.
+induction n; induction m; simpl in |- *; auto with arith.
+Qed.
+
+Lemma le_max_l : forall n m, n <= max n m.
+Proof.
+induction n; intros; simpl in |- *; auto with arith.
+elim m; intros; simpl in |- *; auto with arith.
+Qed.
+
+Lemma le_max_r : forall n m, m <= max n m.
+Proof.
+induction n; simpl in |- *; auto with arith.
+induction m; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve max_r max_l le_max_l le_max_r: arith v62.
+
+
+(** [max n m] is equal to [n] or [m] *)
+
+Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
+Proof.
+induction n; induction m; simpl in |- *; auto with arith.
+elim (IHn m); intro H; elim H; auto.
+Qed.
+
+Lemma max_case : forall n m (P:nat -> Set), 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.
+Qed.
+
+Lemma max_case2 : forall n m (P:nat -> Prop), 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.
+Qed.
+
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
new file mode 100755
index 00000000..912e7ba3
--- /dev/null
+++ b/theories/Arith/Min.v
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*  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: Min.v,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Arith.
+
+Open Local Scope nat_scope.
+
+Implicit Types m n : nat.
+
+(** minimum of two natural numbers *)
+
+Fixpoint min n m {struct n} : nat :=
+  match n, m with
+  | O, _ => 0
+  | S n', O => 0
+  | S n', S m' => S (min n' m')
+  end.
+
+(** Simplifications of [min] *)
+
+Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
+Proof.
+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.
+Qed.
+
+(** [min] and [le] *)
+
+Lemma min_l : forall n m, n <= m -> min n m = n.
+Proof.
+induction n; induction m; simpl in |- *; auto with arith.
+Qed.
+
+Lemma min_r : forall n m, m <= n -> min n m = m.
+Proof.
+induction n; induction m; simpl in |- *; auto with arith.
+Qed.
+
+Lemma le_min_l : forall n m, min n m <= n.
+Proof.
+induction n; intros; simpl in |- *; auto with arith.
+elim m; intros; simpl in |- *; auto with arith.
+Qed.
+
+Lemma le_min_r : forall n m, min n m <= m.
+Proof.
+induction n; simpl in |- *; auto with arith.
+induction m; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve min_l min_r le_min_l le_min_r: arith v62.
+
+(** [min n m] is equal to [n] or [m] *)
+
+Lemma min_dec : forall n m, {min n m = n} + {min n m = m}.
+Proof.
+induction n; induction m; simpl in |- *; auto with arith.
+elim (IHn m); intro H; elim H; auto.
+Qed.
+
+Lemma min_case : forall n m (P:nat -> Set), P n -> P m -> P (min n m).
+Proof.
+induction n; simpl in |- *; auto with arith.
+induction m; intros; simpl in |- *; auto with arith.
+pattern (min n m) in |- *; apply IHn; auto with arith.
+Qed.
+
+Lemma min_case2 : forall n m (P:nat -> Prop), P n -> P m -> P (min n m).
+Proof.
+induction n; simpl in |- *; auto with arith.
+induction m; intros; simpl in |- *; auto with arith.
+pattern (min n m) in |- *; apply IHn; auto with arith.
+Qed.
\ No newline at end of file
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
new file mode 100755
index 00000000..ba9a46ad
--- /dev/null
+++ b/theories/Arith/Minus.v
@@ -0,0 +1,123 @@
+(************************************************************************)
+(*  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: Minus.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+(** Subtraction (difference between two natural numbers) *)
+
+Require Import Lt.
+Require Import Le.
+
+Open Local Scope nat_scope.
+
+Implicit Types m n p : nat.
+
+(** 0 is right neutral *)
+
+Lemma minus_n_O : forall n, n = n - 0.
+Proof.
+induction n; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve minus_n_O: arith v62.
+
+(** Permutation with successor *)
+
+Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
+Proof.
+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.
+Qed.
+
+(** Diagonal *)
+
+Lemma minus_n_n : forall n, 0 = n - n.
+Proof.
+induction n; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve minus_n_n: arith v62.
+
+(** Simplification *)
+
+Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
+Proof.
+  induction p; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve minus_plus_simpl_l_reverse: arith v62.
+
+(** Relation with plus *)
+
+Lemma plus_minus : forall n m p, n = m + p -> p = n - m.
+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.
+Qed.
+Hint Immediate plus_minus: arith v62.
+
+Lemma minus_plus : forall n m, n + m - n = m.
+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.
+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.
+Qed.
+Hint Resolve le_plus_minus_r: arith v62.
+
+(** 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 ].
+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.
+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.
+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
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
new file mode 100755
index 00000000..abfade57
--- /dev/null
+++ b/theories/Arith/Mult.v
@@ -0,0 +1,211 @@
+(************************************************************************)
+(*  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: Mult.v,v 1.21.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Export Plus.
+Require Export Minus.
+Require Export Lt.
+Require Export Le.
+
+Open Local Scope nat_scope.
+
+Implicit Types m n p : nat.
+
+(** Zero property *)
+
+Lemma mult_0_r : forall n, n * 0 = 0.
+Proof.
+intro; symmetry  in |- *; apply mult_n_O.
+Qed.
+
+Lemma mult_0_l : forall n, 0 * n = 0.
+Proof.
+reflexivity.
+Qed.
+
+(** Distributivity *)
+
+Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
+Proof.
+intros; elim n; simpl in |- *; intros; auto with arith.
+elim plus_assoc; elim H; auto with arith.
+Qed.
+Hint Resolve mult_plus_distr_r: arith v62.
+
+Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
+Proof.
+  induction n. trivial.
+  intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4.
+Qed.
+
+Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
+Proof.
+intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros;
+ auto with arith.
+elim minus_plus_simpl_l_reverse; auto with arith.
+Qed.
+Hint Resolve mult_minus_distr_r: arith v62.
+
+(** Associativity *)
+
+Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
+Proof.
+intros; elim n; intros; simpl in |- *; auto with arith.
+rewrite mult_plus_distr_r.
+elim H; auto with arith.
+Qed.
+Hint Resolve mult_assoc_reverse: arith v62.
+
+Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
+Proof.
+auto with arith.
+Qed.
+Hint Resolve mult_assoc: arith v62.
+
+(** Commutativity *)
+
+Lemma mult_comm : forall n m, n * m = m * n.
+Proof.
+intros; elim n; intros; simpl in |- *; auto with arith.
+elim mult_n_Sm.
+elim H; apply plus_comm.
+Qed.
+Hint Resolve mult_comm: arith v62.
+
+(** 1 is neutral *)
+
+Lemma mult_1_l : forall n, 1 * n = n.
+Proof.
+simpl in |- *; auto with arith.
+Qed.
+Hint Resolve mult_1_l: arith v62.
+
+Lemma mult_1_r : forall n, n * 1 = n.
+Proof.
+intro; elim mult_comm; auto with arith.
+Qed.
+Hint Resolve mult_1_r: arith v62.
+
+(** Compatibility with orders *)
+
+Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
+Proof.
+induction m; simpl in |- *; auto with arith.
+Qed.
+Hint Resolve mult_O_le: arith v62.
+
+Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
+Proof.
+  induction p as [| p IHp]. intros. simpl in |- *. apply le_n.
+  intros. simpl in |- *. apply plus_le_compat. assumption.
+  apply IHp. assumption.
+Qed.
+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.
+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.
+Qed.
+
+Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
+Proof.
+  intro m; induction m. intros. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption.
+  intros. exact (plus_lt_compat _ _ _ _ H (IHm _ _ H)).
+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.
+Qed.
+
+Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
+Proof.
+  intros m n p H. elim (le_or_lt n p). trivial.
+  intro H0. cut (S m * n < S m * n). intro. elim (lt_irrefl _ H1).
+  apply le_lt_trans with (m := S m * p). assumption.
+  apply mult_S_lt_compat_l. assumption.
+Qed.
+
+(** 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.
+Qed.
+
+
+(** Tail-recursive mult *)
+
+(** [tail_mult] is an alternative definition for [mult] which is 
+    tail-recursive, whereas [mult] is not. This can be useful 
+    when extracting programs. *)
+
+Fixpoint mult_acc (s:nat) m n {struct n} : nat :=
+  match n with
+  | 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.
+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.
+Qed.
+
+(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] 
+    and [mult] and simplify *)
+
+Ltac tail_simpl :=
+  repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
+   simpl in |- *. 
\ No newline at end of file
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
new file mode 100755
index 00000000..01204ee6
--- /dev/null
+++ b/theories/Arith/Peano_dec.v
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  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: Peano_dec.v,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+Require Import Decidable.
+
+Open Local Scope nat_scope.
+
+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.
+Defined.
+
+Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
+Proof.
+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.
+Defined.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
new file mode 100755
index 00000000..e4ac631e
--- /dev/null
+++ b/theories/Arith/Plus.v
@@ -0,0 +1,202 @@
+(************************************************************************)
+(*  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: Plus.v,v 1.18.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+(** Properties of addition *)
+
+Require Import Le.
+Require Import Lt.
+
+Open Local Scope nat_scope.
+
+Implicit Types m n p q : nat.
+
+(** Zero is neutral *)
+
+Lemma plus_0_l : forall n, 0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Lemma plus_0_r : forall n, n + 0 = n.
+Proof.
+intro; symmetry  in |- *; apply plus_n_O.
+Qed.
+
+(** 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.
+Qed.
+Hint Immediate plus_comm: arith v62.
+
+(** 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.
+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.
+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.
+Qed.
+
+Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p).
+Proof.
+auto with arith.
+Qed.
+Hint Resolve plus_assoc_reverse: arith v62.
+
+(** 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.
+Qed.
+
+Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
+Proof.
+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.
+Qed.
+
+(** 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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+Qed.
+
+Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
+Proof.
+  unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. rewrite plus_Snm_nSm.
+  apply plus_le_compat; assumption.
+Qed.
+
+Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
+Proof.
+  unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. apply plus_le_compat; assumption.
+Qed.
+
+Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Proof.
+  intros. apply plus_lt_le_compat. assumption.
+  apply lt_le_weak. assumption.
+Qed.
+
+(** Inversion lemmas *)
+
+Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0.
+Proof.
+  intro m; destruct m as [| n]; auto.
+  intros. discriminate H.
+Qed.
+
+Definition plus_is_one :
+  forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
+Proof.
+  intro m; destruct m as [| n]; auto.
+  destruct n; auto.
+  intros. 
+  simpl in H. discriminate H.
+Defined.
+
+(** Derived properties *)
+
+Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).
+Proof.
+  intros m n p q. 
+  rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q).
+  rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc.
+Qed.
+
+(** Tail-recursive plus *)
+
+(** [tail_plus] is an alternative definition for [plus] which is 
+    tail-recursive, whereas [plus] is not. This can be useful
+    when extracting programs. *)
+
+Fixpoint plus_acc q n {struct n} : nat :=
+  match n with
+  | O => q
+  | S p => plus_acc (S q) p
+  end.
+
+Definition tail_plus n m := plus_acc m n.
+
+Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
+unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto.
+intro m; rewrite <- IHn; simpl in |- *; auto.
+Qed.
\ No newline at end of file
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
new file mode 100755
index 00000000..8bf237b5
--- /dev/null
+++ b/theories/Arith/Wf_nat.v
@@ -0,0 +1,206 @@
+(************************************************************************)
+(*  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: Wf_nat.v,v 1.16.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)
+
+(** Well-founded relations and natural numbers *)
+
+Require Import Lt.
+
+Open Local Scope nat_scope.
+
+Implicit Types m n p : nat.
+
+Section Well_founded_Nat.
+
+Variable A : Set.
+
+Variable f : A -> nat.
+Definition ltof (a b:A) := f a < f b.
+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.
+Qed.
+
+Theorem well_founded_gtof : well_founded gtof.
+Proof well_founded_ltof.
+
+(** It is possible to directly prove the induction principle going
+   back to primitive recursion on natural numbers ([induction_ltof1])
+   or to use the previous lemmas to extract a program with a fixpoint
+   ([induction_ltof2]) 
+
+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 : [[
+   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.
+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.
+Proof.
+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.
+Proof.
+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.
+Proof.
+exact induction_ltof2.
+Defined.
+
+(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
+    then [R] is well-founded. *)
+
+Variable R : A -> A -> Prop.
+
+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.
+Qed.
+
+End Well_founded_Nat.
+
+Lemma lt_wf : well_founded lt.
+Proof well_founded_ltof nat (fun m => m).
+
+Lemma lt_wf_rec1 :
+ forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+Proof.
+exact
+ (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) =>
+    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.
+Proof.
+exact
+ (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) =>
+    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.
+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.
+Proof.
+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.
+Proof lt_wf_ind.
+
+Lemma lt_wf_double_rec :
+ forall P:nat -> nat -> Set,
+   (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.
+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 (q:nat), p < n -> P p q) ->
+      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
+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.
+intros x [n fxn]; generalize x fxn; clear x fxn.
+pattern n in |- *; apply lt_wf_ind; intros.
+constructor; intros.
+case (F_compat y x); trivial; intros.
+apply (H x0); auto.
+Qed.
+
+Theorem well_founded_inv_lt_rel_compat : well_founded R.
+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.
+Qed.
\ No newline at end of file
diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex
new file mode 100755
index 00000000..655de34c
--- /dev/null
+++ b/theories/Arith/intro.tex
@@ -0,0 +1,55 @@
+\section{Arith}\label{Arith}
+
+The {\tt Arith} library deals with various arithmetical notions and 
+their properties.
+
+\subsection*{Standard {\tt Arith} library}
+
+The following files are automatically loaded by {\tt Require Arith}.
+
+\begin{itemize}
+
+\item {\tt Le.v} states and proves properties of the large order {\tt le}.
+
+\item {\tt Lt.v} states and proves properties of the strict order {\tt 
+lt} (especially, the relationship with {\tt le}).
+
+\item {\tt Plus.v} states and proves properties on the addition.
+
+\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}.
+
+\item {\tt Minus.v} defines the difference on 
+{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is 
+{\tt O} if {\tt n} $<$ {\tt p}.
+
+\item {\tt Mult.v} states and proves properties on the multiplication.
+
+\item {\tt Between.v} defines modalities on {\tt nat} and proves properties 
+of them.
+
+\end{itemize}
+
+\subsection*{Additional {\tt Arith} library}
+
+\begin{itemize}
+
+\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state
+and prove various decidability results on {\tt nat}.
+
+\item {\tt Wf\_nat.v} states and proves various induction and recursion 
+principles on {\tt nat}. Especially, recursion for objects measurable by 
+a natural number and recursion on {\tt nat * nat} are provided.
+
+\item {\tt Min.v} defines the minimum of two natural numbers and proves 
+properties of it. 
+
+\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows 
+the equivalence with Leibniz' equality.
+
+\item {\tt Euclid.v} proves that the euclidean
+division specification is realisable. Conversely, {\tt Div.v} exhibits
+two different algorithms and semi-automatically reconstruct the proof of
+their correctness. These files emphasize the extraction of program vs
+reconstruction of proofs paradigm.
+
+\end{itemize}