mise sous CVS du repertoire theories/Arith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 1495 insertions, 0 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
new file mode 100755
index 000000000..ab3a00ce7
--- /dev/null
+++ b/theories/Arith/Arith.v
@@ -0,0 +1,30 @@
+
+(* $Id$ *)
+
+Require Export Le.
+Require Export Lt.
+Require Export Plus.
+Require Export Gt.
+Require Export Minus.
+Require Export Mult.
+Require Export Between.
+Require Export Minus.
+
+Axiom My_special_variable : nat -> nat.
+Declare ML Module "g_natsyntax".
+
+Grammar nat number :=.
+
+Grammar command command10 :=
+  natural_nat [ nat:number($c) ] -> [$c].
+
+Grammar command atomic_pattern :=
+  natural_pat [ nat:number($c) ] -> [$c].
+
+Syntax constr
+  level  0:
+ myspecialvariable [<<My_special_variable>>] -> ["S"];
+  level 10:
+  S [<<(S $p)>>] -> [$p:"nat_printer"]
+| O [<<O>>] -> [ "0" ]
+.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
new file mode 100755
index 000000000..70307311b
--- /dev/null
+++ b/theories/Arith/Between.v
@@ -0,0 +1,173 @@
+
+(* $Id$ *)
+
+Require Le.
+Require Lt.
+
+Section Between.
+Variables P,Q : nat -> Prop.
+
+Inductive between [k:nat] : nat -> Prop
+ := bet_emp : (between k k)
+ | bet_S : (l:nat)(between k l)->(P l)->(between k (S l)).
+
+Hint constr_between : arith v62 := Constructors between.
+
+Lemma bet_eq : (k,l:nat)(l=k)->(between k l).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Hints Resolve bet_eq : arith v62.
+
+Lemma between_le : (k,l:nat)(between k l)->(le k l).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+Hints Immediate between_le : arith v62.
+
+Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l).
+Proof.
+Induction 1.
+Intros; Absurd (le (S k) k); Auto with arith.
+Induction 1; Auto with arith.
+Qed.
+Hints Resolve between_Sk_l : arith v62.
+
+Lemma between_restr : 
+  (k,l,m:nat)(le k l)->(le l m)->(between k m)->(between l m).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Inductive exists [k:nat] : nat -> Prop
+ := exists_S : (l:nat)(exists k l)->(exists k (S l))
+ | exists_le: (l:nat)(le k l)->(Q l)->(exists k (S l)).
+
+Hint constr_exists : arith v62 := Constructors exists.
+
+Lemma exists_le_S : (k,l:nat)(exists k l)->(le (S k) l).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Lemma exists_lt : (k,l:nat)(exists k l)->(lt k l).
+Proof exists_le_S.
+Hints Immediate exists_le_S exists_lt : arith v62.
+
+Lemma exists_S_le : (k,l:nat)(exists k (S l))->(le k l).
+Proof.
+Intros; Apply le_S_n; Auto with arith.
+Qed.
+Hints Immediate exists_S_le : arith v62.
+
+Definition in_int := [p,q,r:nat](le p r)/\(lt r q).
+
+Lemma in_int_intro : (p,q,r:nat)(le p r)->(lt r q)->(in_int p q r).
+Proof.
+Red; Auto with arith.
+Qed.
+Hints Resolve in_int_intro : arith v62.
+
+Lemma in_int_lt : (p,q,r:nat)(in_int p q r)->(lt p q).
+Proof.
+Induction 1; Intros.
+Apply le_lt_trans with r; Auto with arith.
+Qed.
+
+Lemma in_int_p_Sq : 
+  (p,q,r:nat)(in_int p (S q) r)->((in_int p q r) \/ <nat>r=q).
+Proof.
+Induction 1; Intros.
+Elim (le_lt_or_eq r q); Auto with arith.
+Qed.
+
+Lemma in_int_S : (p,q,r:nat)(in_int p q r)->(in_int p (S q) r).
+Proof.
+Induction 1;Auto with arith.
+Qed.
+Hints Resolve in_int_S : arith v62.
+
+Lemma in_int_Sp_q : (p,q,r:nat)(in_int (S p) q r)->(in_int p q r).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+Hints Immediate in_int_Sp_q : arith v62.
+
+Lemma between_in_int : (k,l:nat)(between k l)->(r:nat)(in_int k l r)->(P r).
+Proof.
+Induction 1; Intros.
+Absurd (lt k k); Auto with arith.
+Apply in_int_lt with r; Auto with arith.
+Elim (in_int_p_Sq k l0 r); Intros; Auto with arith.
+Rewrite H4; Trivial with arith.
+Qed.
+
+Lemma in_int_between : 
+  (k,l:nat)(le k l)->((r:nat)(in_int k l r)->(P r))->(between k l).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Lemma exists_in_int : 
+  (k,l:nat)(exists k l)->(EX m:nat | (in_int k l m) & (Q m)).
+Proof.
+Induction 1.
+Induction 2; Intros p inp Qp; Exists p; Auto with arith.
+Intros; Exists l0; Auto with arith.
+Qed.
+
+Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l).
+Proof.
+Induction 1; Intros.
+Elim H1; Auto with arith.
+Qed.
+
+Lemma between_or_exists : 
+  (k,l:nat)(le k l)->((n:nat)(in_int k l n)->((P n)\/(Q n)))
+     ->((between k l)\/(exists k l)).
+Proof.
+Induction 1; Intros; Auto with arith.
+Elim H1; Intro; Auto with arith.
+Elim (H2 m); Auto with arith.
+Qed.
+
+Lemma between_not_exists : (k,l:nat)(between k l)->
+     ((n:nat)(in_int k l n) -> (P n) -> ~(Q n))
+     -> ~(exists k l).
+Proof.
+Induction 1; Red; Intros.
+Absurd (lt k k); Auto with arith.
+Absurd (Q l0); Auto with arith.
+Elim (exists_in_int k (S l0)); Auto with arith; Intros l' inl' Ql'.
+Replace l0 with l'; Auto with arith.
+Elim inl'; Intros.
+Elim (le_lt_or_eq l' l0); Auto with arith; Intros.
+Absurd (exists k l0); Auto with arith.
+Apply in_int_exists with l'; Auto with arith.
+Qed.
+
+Inductive nth [init:nat] : nat->nat->Prop
+  := nth_O : (nth init init O)
+  | nth_S : (k,l:nat)(n:nat)(nth init k n)->(between (S k) l)
+                        ->(Q l)->(nth init l (S n)).
+
+Lemma nth_le : (init,l,n:nat)(nth init l n)->(le init l).
+Proof.
+Induction 1; Intros; Auto with arith.
+Apply le_trans with (S k); Auto with arith.
+Qed.
+
+Definition eventually := [n:nat](EX k:nat | (le k n) & (Q k)).
+
+Lemma event_O : (eventually O)->(Q O).
+Proof.
+Induction 1; Intros.
+Replace O with x; Auto with arith.
+Qed.
+
+End Between.
+
+Hints Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le 
+ in_int_S in_int_intro : arith v62. 
+Hints 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
new file mode 100755
index 000000000..343b408b1
--- /dev/null
+++ b/theories/Arith/Compare.v
@@ -0,0 +1,49 @@
+
+(* $Id$ *)
+
+(********************************************)
+(* equality is decidable on nat             *)
+(********************************************)
+
+
+Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q)->~(q=p).
+Proof sym_not_eq.
+Hints Immediate not_eq_sym : arith.
+
+Require Arith.
+Require Peano_dec.
+Require Compare_dec.
+
+Definition le_or_le_S := le_le_S_dec.
+
+Definition compare := gt_eq_gt_dec.
+
+Lemma le_dec : (n,m:nat) {le n m} + {le m n}.
+Proof le_ge_dec.
+
+Definition lt_or_eq := [n,m:nat]{(gt m n)}+{n=m}.
+
+Lemma le_decide : (n,m:nat)(le n m)->(lt_or_eq n m).
+Proof le_lt_eq_dec.
+
+Lemma le_le_S_eq : (p,q:nat)(le p q)->((le (S p) q)\/(p=q)).
+Proof le_lt_or_eq.
+
+(* By special request of G. Kahn - Used in Group Theory *)
+Lemma discrete_nat : (m, n: nat) (lt m n) ->
+   (S m) = n \/ (EX r: nat | n = (S (S (plus m 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 (minus n (S (S m))); Simpl.
+Rewrite (plus_sym m (minus n (S (S m)))).
+Rewrite (plus_n_Sm (minus n (S (S m))) m).
+Rewrite (plus_n_Sm (minus n (S (S m))) (S m)).
+Rewrite (plus_sym (minus 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 000000000..0e49083b9
--- /dev/null
+++ b/theories/Arith/Compare_dec.v
@@ -0,0 +1,47 @@
+
+(* $Id$ *)
+
+Require Le.
+Require Lt.
+
+Theorem zerop : (n:nat){n=O}+{lt O n}.
+Destruct n; Auto with arith.
+Save.
+
+Theorem lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
+Proof.
+Induction n; Induction m; Auto with arith.
+Intros q H'; Elim (H q).
+Induction 1; Auto with arith.
+Auto with arith.
+Qed.
+
+Lemma gt_eq_gt_dec : (n,m:nat)({(gt m n)}+{n=m})+{(gt n m)}.
+Proof lt_eq_lt_dec.
+
+Lemma le_lt_dec : (n,m:nat) {le n m} + {lt m n}.
+Proof.
+Induction n.
+Auto with arith.
+Induction m.
+Auto with arith.
+Intros q H'; Elim (H q); Auto with arith.
+Qed.
+
+Lemma le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
+Proof le_lt_dec.
+
+Lemma le_ge_dec : (n,m:nat) {le n m} + {ge n m}.
+Proof.
+Intros; Elim (le_lt_dec n m); Auto with arith.
+Qed.
+
+Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
+Proof le_lt_dec.
+
+
+Theorem le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}).
+Proof.
+Intros; Elim (lt_eq_lt_dec n m); Auto with arith.
+Intros; Absurd (lt m n); Auto with arith.
+Qed.
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
new file mode 100755
index 000000000..c6ea0a6f2
--- /dev/null
+++ b/theories/Arith/Div.v
@@ -0,0 +1,52 @@
+
+(* $Id$ *)
+
+(* Euclidean division *)
+
+Require Le.
+Require Euclid_def.
+Require Compare_dec.
+
+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.
+Save.
+
+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.
+Save.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
new file mode 100644
index 000000000..b1409b182
--- /dev/null
+++ b/theories/Arith/Div2.v
@@ -0,0 +1,156 @@
+
+(* $Id$ *)
+
+Require Lt.
+Require Plus.
+Require Compare_dec.
+Require Even.
+
+(* Here we define n/2 and prove some of its properties *)
+
+Fixpoint div2 [n:nat] : nat :=
+  Cases n of
+    O => O
+  | (S O) => O
+  | (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 : (P:nat->Prop)
+  (P O) -> (P (S O)) -> ((n:nat)(P n)->(P (S (S n)))) -> (n:nat)(P n).
+Proof.
+Intros.
+Cut (n:nat)(P n)/\(P (S n)).
+Intros. Elim (H2 n). Auto with arith.
+
+Induction n0. Auto with arith.
+Intros. (Elim H2; Auto with arith).
+Save.
+
+(* 0 <n  =>  n/2 < n *)
+
+Lemma lt_div2 : (n:nat) (lt O n) -> (lt (div2 n) n).
+Proof.
+Intro n. Pattern n. Apply ind_0_1_SS.
+Intro. Inversion H.
+Auto with arith.
+Intros. Simpl.
+Case (zerop n0).
+Intro. Rewrite e. Auto with arith.
+Auto with arith.
+Save.
+
+Hints Resolve lt_div2 : arith.
+
+(* Properties related to the parity *)
+
+Lemma even_odd_div2 : (n:nat) 
+  ((even n)<->(div2 n)=(div2 (S n))) /\ ((odd n)<->(S (div2 n))=(div2 (S n))).
+Proof.
+Intro n. Pattern n. Apply ind_0_1_SS.
+(* n  = 0 *)
+Split. Split; Auto with arith. 
+Split. Intro H. Inversion H.
+Intro H.  Absurd (S (div2 O))=(div2 (S O)); Auto with arith.
+(* n = 1 *)
+Split. Split. Intro. Inversion H. Inversion H1.
+Intro H.  Absurd (div2 (S O))=(div2 (S (S O))).
+Simpl. Discriminate. Assumption.
+Split; Auto with arith.
+(* n = (S (S n')) *)
+Intros. Decompose [and] H. Unfold iff in H1 H2.
+Decompose [and] H1. Decompose [and] H2. Clear H H1 H2.
+Split; Split; Auto with arith.
+Intro H. Inversion H. Inversion H1.
+Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith.
+Intro H. Inversion H. Inversion H1.
+Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith.
+Save.
+
+(* Specializations *)
+
+Lemma even_div2 : (n:nat) (even n) -> (div2 n)=(div2 (S n)).
+Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_div2 n))).
+
+Lemma div2_even : (n:nat) (div2 n)=(div2 (S n)) -> (even n).
+Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_div2 n))).
+
+Lemma odd_div2 : (n:nat) (odd n) -> (S (div2 n))=(div2 (S n)).
+Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_div2 n))).
+
+Lemma div2_odd : (n:nat) (S (div2 n))=(div2 (S n)) -> (odd n).
+Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_div2 n))).
+
+Hints Resolve even_div2 div2_even odd_div2 div2_odd : arith.
+
+(* Properties related to the double (2n) *)
+
+Definition double := [n:nat](plus n n).
+
+Hints Unfold double : arith.
+
+Lemma double_S : (n:nat) (double (S n))=(S (S (double n))).
+Proof.
+Intro. Unfold double. Simpl. Auto with arith.
+Save.
+
+Hints Resolve double_S : arith.
+
+Lemma even_odd_double : (n:nat) 
+  ((even n)<->n=(double (div2 n))) /\ ((odd n)<->n=(S (double (div2 n)))).
+Proof.
+Intro n. Pattern n. Apply ind_0_1_SS.
+(* n = 0 *)
+Split; Split; Auto with arith.
+Intro H. Inversion H.
+(* n = 1 *)
+Split; Split; Auto with arith.
+Intro H. Inversion H. Inversion H1.
+(* n = (S (S n')) *)
+Intros. Decompose [and] H. Unfold iff in H1 H2.
+Decompose [and] H1. Decompose [and] H2. Clear H H1 H2.
+Split; Split.
+Intro H. Inversion H. Inversion H1.
+Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
+Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
+Intro H. Inversion H. Inversion H1.
+Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
+Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
+Save.
+
+
+(* Specializations *)
+
+Lemma even_double : (n:nat) (even n) -> n=(double (div2 n)).
+Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_double n))).
+
+Lemma double_even : (n:nat) n=(double (div2 n)) -> (even n).
+Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_double n))).
+
+Lemma odd_double : (n:nat) (odd n) -> n=(S (double (div2 n))).
+Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_double n))).
+
+Lemma double_odd : (n:nat) n=(S (double (div2 n))) -> (odd n).
+Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_double n))).
+
+Hints 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 : (n:nat) (even n) -> { p:nat | n=(double p) }.
+Proof.
+Intros n H. Exists (div2 n). Auto with arith.
+Save.
+
+Lemma odd_S2n : (n:nat) (odd n) -> { p:nat | n=(S (double p)) }.
+Proof.
+Intros n H. Exists (div2 n). Auto with arith.
+Save.
+
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
new file mode 100755
index 000000000..0f641e9b7
--- /dev/null
+++ b/theories/Arith/EqNat.v
@@ -0,0 +1,53 @@
+
+(* $Id$ *)
+
+(**************************************************************************)
+(*                    Equality on natural numbers                         *)
+(**************************************************************************)
+
+Fixpoint  eq_nat [n:nat] : nat -> Prop :=
+  [m:nat]Cases n m of 
+                O      O     => True
+             |  O     (S _)  => False
+             | (S _)   O     => False
+             | (S n1) (S m1) => (eq_nat n1 m1)
+          end.
+
+Theorem eq_nat_refl : (n:nat)(eq_nat n n).
+Induction n; Simpl; Auto.
+Qed.
+Hints Resolve eq_nat_refl : arith v62.
+
+Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m).
+Induction 1; Trivial with arith.
+Qed.
+Hints Immediate eq_eq_nat : arith v62.
+
+Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m).
+Induction n; Induction m; Simpl; (Contradiction Orelse Auto with arith).
+Qed.
+Hints Immediate eq_nat_eq : arith v62.
+
+Theorem eq_nat_elim : (n:nat)(P:nat->Prop)(P n)->(m:nat)(eq_nat n m)->(P m).
+Intros; Replace m with n; Auto with arith.
+Qed.
+
+Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}.
+Induction n.
+Destruct m.
+Auto with arith.
+(Intro; Right; Red; Trivial with arith).
+Destruct m.
+(Right; Red; Auto with arith).
+Intros.
+Simpl.
+Apply H.
+Defined.
+
+Fixpoint  beq_nat [n:nat] : nat -> bool :=
+  [m:nat]Cases n m of 
+                O      O     => true
+             |  O     (S _)  => false
+             | (S _)   O     => false
+             | (S n1) (S m1) => (beq_nat n1 m1)
+          end.
diff --git a/theories/Arith/Euclid_def.v b/theories/Arith/Euclid_def.v
new file mode 100755
index 000000000..292816f45
--- /dev/null
+++ b/theories/Arith/Euclid_def.v
@@ -0,0 +1,7 @@
+
+(* $Id$ *)
+
+Require Export Mult.
+
+Inductive diveucl [a,b:nat] : Set 
+      := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b).
diff --git a/theories/Arith/Euclid_proof.v b/theories/Arith/Euclid_proof.v
new file mode 100755
index 000000000..75c98c55e
--- /dev/null
+++ b/theories/Arith/Euclid_proof.v
@@ -0,0 +1,49 @@
+
+(* $Id$ *)
+
+Require Euclid_def.
+Require Compare_dec.
+Require Wf_nat.
+
+Lemma eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b).
+Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0.
+Elim (le_gt_dec b n).
+Intro lebn.
+Elim (H0 (minus n b)); Auto with arith.
+Intros q r g e.
+Apply divex with (S q) r; Simpl; Auto with arith.
+Elim plus_assoc_l.
+Elim e; Auto with arith.
+Intros gtbn.
+Apply divex with O n; Simpl; Auto with arith.
+Save.
+
+Lemma quotient : (b:nat)(gt b O)->
+     (a:nat){q:nat|(EX r:nat | (a=(plus (mult q b) r))/\(gt b r))}.
+Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0.
+Elim (le_gt_dec b n).
+Intro lebn.
+Elim (H0 (minus n b)); Auto with arith.
+Intros q Hq; Exists (S q).
+Elim Hq; Intros r Hr.
+Exists r; Simpl; Elim Hr; Intros.
+Elim plus_assoc_l.
+Elim H1; Auto with arith.
+Intros gtbn.
+Exists O; Exists n; Simpl; Auto with arith.
+Save.
+
+Lemma modulo : (b:nat)(gt b O)->
+     (a:nat){r:nat|(EX q:nat | (a=(plus (mult q b) r))/\(gt b r))}.
+Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0.
+Elim (le_gt_dec b n).
+Intro lebn.
+Elim (H0 (minus n b)); Auto with arith.
+Intros r Hr; Exists r.
+Elim Hr; Intros q Hq.
+Elim Hq; Intros; Exists (S q); Simpl.
+Elim plus_assoc_l.
+Elim H1; Auto with arith.
+Intros gtbn.
+Exists n; Exists O; Simpl; Auto with arith.
+Save.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
new file mode 100644
index 000000000..a79a4d267
--- /dev/null
+++ b/theories/Arith/Even.v
@@ -0,0 +1,39 @@
+
+(* $Id$ *)
+
+(* 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.
+ *)
+
+Inductive even : nat->Prop :=
+    even_O : (even O)
+  | even_S : (n:nat)(odd n)->(even (S n))
+with odd : nat->Prop :=
+    odd_S : (n:nat)(even n)->(odd (S n)).
+
+Hint constr_even : arith := Constructors even.
+Hint constr_odd : arith := Constructors odd.
+
+Lemma even_or_odd : (n:nat) (even n)\/(odd n).
+Proof.
+Induction n.
+Auto with arith.
+Intros n' H. Elim H; Auto with arith.
+Save.
+
+Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }.
+Proof.
+Induction n.
+Auto with arith.
+Intros n' H. Elim H; Auto with arith.
+Save.
+
+Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False.
+Proof.
+Induction n.
+Intros. Inversion H0.
+Intros. Inversion H0. Inversion H1. Auto with arith.
+Save.
+
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
new file mode 100755
index 000000000..904aac7bd
--- /dev/null
+++ b/theories/Arith/Gt.v
@@ -0,0 +1,121 @@
+
+(* $Id$ *)
+
+Require Le.
+Require Lt.
+Require Plus.
+
+Theorem gt_Sn_O : (n:nat)(gt (S n) O).
+Proof.
+  Auto with arith.
+Qed.
+Hints Resolve gt_Sn_O : arith v62.
+
+Theorem gt_Sn_n : (n:nat)(gt (S n) n).
+Proof.
+  Auto with arith.
+Qed.
+Hints Resolve gt_Sn_n : arith v62.
+
+Theorem le_S_gt : (n,m:nat)(le (S n) m)->(gt m n).
+Proof.
+  Auto with arith.
+Qed.
+Hints Immediate le_S_gt : arith v62.
+
+Theorem gt_n_S : (n,m:nat)(gt n m)->(gt (S n) (S m)).
+Proof.
+  Auto with arith.
+Qed.
+Hints Resolve gt_n_S : arith v62.
+
+Theorem gt_trans_S : (n,m,p:nat)(gt (S n) m)->(gt m p)->(gt n p).
+Proof.
+  Red; Intros; Apply lt_le_trans with m; Auto with arith.
+Qed.
+
+Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p).
+Proof.
+  Red; Intros; Apply lt_le_trans with m; Auto with arith.
+Qed.
+
+Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p).
+Proof.
+  Red; Intros; Apply le_lt_trans with m; Auto with arith.
+Qed.
+
+Hints Resolve gt_trans_S le_gt_trans gt_le_trans : arith v62.
+
+Lemma le_not_gt : (n,m:nat)(le n m) -> ~(gt n m).
+Proof le_not_lt.
+Hints Resolve le_not_gt : arith v62.
+
+Lemma gt_antirefl : (n:nat)~(gt n n).
+Proof lt_n_n.
+Hints Resolve gt_antirefl : arith v62.
+
+Lemma gt_not_sym : (n,m:nat)(gt n m) -> ~(gt m n).
+Proof [n,m:nat](lt_not_sym m n).
+
+Lemma gt_not_le : (n,m:nat)(gt n m) -> ~(le n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve gt_not_sym gt_not_le : arith v62.
+
+Lemma gt_trans : (n,m,p:nat)(gt n m)->(gt m p)->(gt n p).
+Proof.
+  Red; Intros n m p H1 H2.
+  Apply lt_trans with m; Auto with arith.
+Qed.
+
+Lemma gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n).
+Proof.
+  Auto with arith.
+Qed.
+Hints Immediate gt_S_n : arith v62.
+
+Lemma gt_S_le : (n,p:nat)(gt (S p) n)->(le n p).
+Proof.
+  Intros n p; Exact (lt_n_Sm_le n p).
+Qed.
+Hints Immediate gt_S_le : arith v62.
+
+Lemma gt_le_S : (n,p:nat)(gt p n)->(le (S n) p).
+Proof.
+  Auto with arith.
+Qed.
+Hints Resolve gt_le_S : arith v62.
+
+Lemma le_gt_S : (n,p:nat)(le n p)->(gt (S p) n).
+Proof.
+  Auto with arith.
+Qed.
+Hints Resolve le_gt_S : arith v62.
+
+Lemma gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n).
+Proof.
+  Auto with arith.
+Qed.
+Hints Immediate gt_pred : arith v62.
+
+Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(<nat>m=n)).
+Proof.
+  Intros n m H; Unfold gt; Apply le_lt_or_eq; Auto with arith.
+Qed.
+
+Theorem gt_O_eq : (n:nat)((gt n O)\/(<nat>O=n)).
+Proof.
+  Intro n ; Apply gt_S ; Auto with arith.
+Qed.
+
+Lemma simpl_gt_plus_l : (n,m,p:nat)(gt (plus p n) (plus p m))->(gt n m).
+Proof.
+  Red; Intros n m p H; Apply simpl_lt_plus_l with p; Auto with arith.
+Qed.
+
+Lemma gt_reg_l : (n,m,p:nat)(gt n m)->(gt (plus p n) (plus p m)).
+Proof.
+  Auto with arith.
+Qed.
+Hints Resolve gt_reg_l : arith v62.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
new file mode 100755
index 000000000..66c73ff82
--- /dev/null
+++ b/theories/Arith/Le.v
@@ -0,0 +1,109 @@
+
+(* $Id$ *)
+
+(***************************************)
+(* Order on natural numbers            *)
+(***************************************)
+
+Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
+Proof.
+  Induction 1; Auto.
+Qed.
+
+Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p).
+Proof.
+  Induction 2; Auto.
+Qed.
+
+Theorem le_n_Sn : (n:nat)(le n (S n)).
+Proof.
+  Auto.
+Qed.
+
+Theorem le_O_n : (n:nat)(le O n).
+Proof.
+  Induction n ; Auto.
+Qed.
+
+Hints Resolve le_n_S le_n_Sn le_O_n le_n_S le_trans : arith v62.
+
+Theorem le_pred_n : (n:nat)(le (pred n) n).
+Proof.
+Induction n ; Auto with arith.
+Qed.
+Hints Resolve le_pred_n : arith v62.
+
+Theorem le_trans_S : (n,m:nat)(le (S n) m)->(le n m).
+Proof.
+Intros n m H ; Apply le_trans with (S n) ; Auto with arith.
+Qed.
+Hints Immediate le_trans_S : arith v62.
+
+Theorem le_S_n : (n,m:nat)(le (S n) (S m))->(le n m).
+Proof.
+Intros n m H ; Change (le (pred (S n)) (pred (S m))).
+(*  (le (pred (S n)) (pred (S m)))
+    ============================
+      H : (le (S n) (S m))
+      m : nat
+      n : nat *)
+Elim H ; Simpl ; Auto with arith.
+Qed.
+Hints Immediate le_S_n : arith v62.
+
+(* Negative properties *)
+
+Theorem le_Sn_O : (n:nat)~(le (S n) O).
+Proof.
+Red ; Intros n H.
+(*  False
+    ============================
+      H : (lt n O)
+      n : nat *)
+Change (IsSucc O) ; Elim H ; Simpl ; Auto with arith.
+Qed.
+Hints Resolve le_Sn_O : arith v62.
+
+Theorem le_Sn_n : (n:nat)~(le (S n) n).
+Proof.
+Induction n; Auto with arith.
+Qed.
+Hints Resolve le_Sn_n : arith v62.
+
+Theorem le_antisym : (n,m:nat)(le n m)->(le m n)->(n=m).
+Proof.
+Intros n m h ; Elim h ; Auto with arith.
+(*  (m:nat)(le n m)->((le m n)->(n=m))->(le (S m) n)->(n=(S m))
+    ============================
+      h : (le n m)
+      m : nat
+      n : nat *)
+Intros m0 H H0 H1.
+Absurd (le (S m0) m0) ; Auto with arith.
+(*  (le (S m0) m0)
+    ============================
+      H1 : (le (S m0) n)
+      H0 : (le m0 n)->(<nat>n=m0)
+      H : (le n m0)
+      m0 : nat *)
+Apply le_trans with n ; Auto with arith.
+Qed.
+Hints Immediate le_antisym : arith v62.
+
+Theorem le_n_O_eq : (n:nat)(le n O)->(O=n).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate le_n_O_eq : arith v62.
+
+(* A different elimination principle for the order on natural numbers *)
+
+Lemma le_elim_rel : (P:nat->nat->Prop)
+     ((p:nat)(P O p))->
+     ((p,q:nat)(le p q)->(P p q)->(P (S p) (S q)))->
+     (n,m:nat)(le n m)->(P n m).
+Proof.
+Induction n; Auto with arith.
+Intros n' HRec m Le.
+Elim Le; Auto with arith.
+Qed.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
new file mode 100755
index 000000000..4c5167e82
--- /dev/null
+++ b/theories/Arith/Lt.v
@@ -0,0 +1,151 @@
+
+(* $Id$ *)
+
+Require Le.
+
+Theorem lt_n_Sn : (n:nat)(lt n (S n)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_n_Sn : arith v62.
+
+Theorem lt_S : (n,m:nat)(lt n m)->(lt n (S m)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_S : arith v62.
+
+Theorem lt_n_S : (n,m:nat)(lt n m)->(lt (S n) (S m)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_n_S : arith v62.
+
+Theorem lt_S_n : (n,m:nat)(lt (S n) (S m))->(lt n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_S_n : arith v62.
+
+Theorem lt_O_Sn : (n:nat)(lt O (S n)).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve lt_O_Sn : arith v62.
+
+Theorem lt_n_O : (n:nat)~(lt n O).
+Proof le_Sn_O.
+Hints Resolve lt_n_O : arith v62.
+
+Theorem lt_n_n : (n:nat)~(lt n n).
+Proof le_Sn_n.
+Hints Resolve lt_n_n : arith v62.
+
+Lemma S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Lemma lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)).
+Proof.
+Induction 1; Simpl; Auto with arith.
+Qed.
+Hints Immediate lt_pred : arith v62.
+
+Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n).
+Destruct 1; Simpl; Auto with arith.
+Save.
+Hints Resolve lt_pred_n_n : arith v62.
+
+(* Relationship between le and lt *) 
+
+Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_le_S : arith v62.
+
+Theorem lt_n_Sm_le : (n,m:nat)(lt n (S m))->(le n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_n_Sm_le : arith v62.
+
+Theorem le_lt_n_Sm : (n,m:nat)(le n m)->(lt n (S m)).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate le_lt_n_Sm : arith v62.
+
+Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_le_weak : arith v62.
+
+Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).
+Proof.
+Induction n; Auto with arith.
+Intros; Absurd O=O; Trivial with arith.
+Qed.
+Hints Immediate neq_O_lt : arith v62.
+
+Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+Hints Immediate lt_O_neq : arith v62.
+
+(* Transitivity properties *)
+
+Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p).
+Proof.
+Induction 2; Auto with arith.
+Qed.
+
+Theorem lt_le_trans : (n,m,p:nat)(lt n m)->(le m p)->(lt n p).
+Proof.
+Induction 2; Auto with arith.
+Qed.
+
+Theorem le_lt_trans : (n,m,p:nat)(le n m)->(lt m p)->(lt n p).
+Proof.
+Induction 2; Auto with arith.
+Qed.
+
+Hints Resolve lt_trans lt_le_trans le_lt_trans : arith v62.
+
+Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
+Proof.
+Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n).
+Proof.
+Red; Intros n m Lt Le; Exact (le_not_lt m n Le Lt).
+Qed.
+Hints Immediate le_not_lt lt_not_le : arith v62.
+
+Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
+Proof.
+Induction 1; Auto with arith.
+Qed.
+
+Theorem nat_total_order: (m,n: nat) ~ m = n -> (lt m n) \/ (lt n m).
+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.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
new file mode 100755
index 000000000..9f5cf5f63
--- /dev/null
+++ b/theories/Arith/Min.v
@@ -0,0 +1,43 @@
+
+(* $Id$ *)
+
+Require Arith.
+
+(**************************************************************************)
+(*                    minimum of two natural numbers                      *)
+(**************************************************************************)
+
+Fixpoint min [n:nat] : nat -> nat :=  
+[m:nat]Cases n m of
+          O      _     => O
+       | (S n')  O     => O
+       | (S n') (S m') => (S (min n' m'))
+       end.
+
+Lemma min_SS : (n,m:nat)((S (min n m))=(min (S n) (S m))).
+Proof.
+Auto with arith.
+Qed.
+
+Lemma le_min_l : (n,m:nat)(le (min n m) n).
+Proof.
+Induction n; Intros; Simpl; Auto with arith.
+Elim m; Intros; Simpl; Auto with arith.
+Qed.
+Hints Resolve le_min_l : arith v62.
+
+Lemma le_min_r : (n,m:nat)(le (min n m) m).
+Proof.
+Induction n; Simpl; Auto with arith.
+Induction m; Simpl; Auto with arith.
+Qed.
+Hints Resolve le_min_r : arith v62.
+
+(* min n m is equal to n or m *)
+
+Lemma min_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (min n m)).
+Proof.
+Induction n; Simpl; Auto with arith.
+Induction m; Intros; Simpl; Auto with arith.
+Pattern (min n0 n1); Apply H ; Auto with arith.
+Qed.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
new file mode 100755
index 000000000..4594aa74d
--- /dev/null
+++ b/theories/Arith/Minus.v
@@ -0,0 +1,89 @@
+
+(* $Id$ *)
+
+
+(**************************************************************************)
+(*          Subtraction (difference between two natural numbers           *)
+(**************************************************************************)
+
+
+Require Lt.
+Require Le.
+
+Fixpoint minus [n:nat] : nat -> nat := 
+  [m:nat]Cases n m of
+            O    _     =>  O
+         | (S k) O     => (S k)
+         | (S k) (S l) => (minus k l)
+        end. 
+
+Lemma minus_plus_simpl : 
+	(n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).
+Proof.
+  Induction p; Simpl; Auto with arith.
+Qed.
+Hints Resolve minus_plus_simpl : arith v62.
+
+Lemma minus_n_O : (n:nat)(n=(minus n O)).
+Proof.
+Induction n; Simpl; Auto with arith.
+Qed.
+Hints Resolve minus_n_O : arith v62.
+
+Lemma minus_n_n : (n:nat)(O=(minus n n)).
+Proof.
+Induction n; Simpl; Auto with arith.
+Qed.
+Hints Resolve minus_n_n : arith v62.
+
+Lemma plus_minus : (n,m,p:nat)(n=(plus m p))->(p=(minus n m)).
+Proof.
+Intros n m p; Pattern m n; Apply nat_double_ind; Simpl; Intros.
+Replace (minus n0 O) with n0; Auto with arith.
+Absurd O=(S (plus n0 p)); Auto with arith.
+Auto with arith.
+Qed.
+Hints Immediate plus_minus : arith v62.
+
+Lemma minus_plus : (n,m:nat)(minus (plus n m) n)=m.
+Symmetry; Auto with arith.
+Save.
+Hints Resolve minus_plus : arith v62.
+
+Lemma le_plus_minus : (n,m:nat)(le n m)->(m=(plus n (minus m n))).
+Proof.
+Intros n m Le; Pattern n m; Apply le_elim_rel; Simpl; Auto with arith.
+Qed.
+Hints Resolve le_plus_minus : arith v62.
+
+Lemma le_plus_minus_r : (n,m:nat)(le n m)->(plus n (minus m n))=m.
+Proof.
+Symmetry; Auto with arith.
+Qed.
+Hints Resolve le_plus_minus_r : arith v62.
+
+
+Lemma minus_Sn_m : (n,m:nat)(le m n)->((S (minus n m))=(minus (S n) m)).
+Proof.
+Intros n m Le; Pattern m n; Apply le_elim_rel; Simpl; Auto with arith.
+Qed.
+Hints Resolve minus_Sn_m : arith v62.
+
+
+Lemma lt_minus : (n,m:nat)(le m n)->(lt O m)->(lt (minus n m) n).
+Proof.
+Intros n m Le; Pattern m n; Apply le_elim_rel; Simpl; Auto with arith.
+Intros; Absurd (lt O O); Auto with arith.
+Intros p q lepq Hp gtp.
+Elim (le_lt_or_eq O p); Auto with arith.
+Auto with arith.
+Induction 1; Elim minus_n_O; Auto with arith.
+Qed.
+Hints Resolve lt_minus : arith v62.
+
+Lemma lt_O_minus_lt : (n,m:nat)(lt O (minus n m))->(lt m n).
+Proof.
+Intros n m; Pattern n m; Apply nat_double_ind; Simpl; Auto with arith.
+Intros; Absurd (lt O O); Trivial with arith.
+Qed.
+Hints Immediate lt_O_minus_lt : arith v62.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
new file mode 100755
index 000000000..fe80384aa
--- /dev/null
+++ b/theories/Arith/Mult.v
@@ -0,0 +1,60 @@
+
+(* $Id$ *)
+
+Require Export Plus.
+Require Export Minus.
+
+(**********************************************************)
+(* Multiplication                                         *)
+(**********************************************************)
+
+Lemma mult_plus_distr : 
+      (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))).
+Proof.
+Intros; Elim n; Simpl; Intros; Auto with arith.
+Elim plus_assoc_l; Elim H; Auto with arith.
+Qed.
+Hints Resolve mult_plus_distr : arith v62.
+
+Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))).
+Proof.
+Intros; Pattern n m; Apply nat_double_ind; Simpl; Intros; Auto with arith.
+Elim minus_plus_simpl; Auto with arith.
+Qed.
+Hints Resolve mult_minus_distr : arith v62.
+
+Lemma mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)).
+Proof.
+Induction m; Simpl; Auto with arith.
+Qed.
+Hints Resolve mult_O_le : arith v62.
+
+Lemma mult_assoc_r : (n,m,p:nat)((mult (mult n m) p) = (mult n (mult m p))).
+Proof.
+Intros; Elim n; Intros; Simpl; Auto with arith.
+Rewrite mult_plus_distr.
+Elim H; Auto with arith.
+Qed.
+Hints Resolve mult_assoc_r : arith v62.
+
+Lemma mult_assoc_l : (n,m,p:nat)(mult n (mult m p)) = (mult (mult n m) p).
+Auto with arith.
+Save.
+Hints Resolve mult_assoc_l : arith v62.
+
+Lemma mult_1_n : (n:nat)(mult (S O) n)=n.
+Simpl; Auto with arith.
+Save.
+Hints Resolve mult_1_n : arith v62.
+
+Lemma mult_sym : (n,m:nat)(mult n m)=(mult m n).
+Intros; Elim n; Intros; Simpl; Auto with arith.
+Elim mult_n_Sm.
+Elim H; Apply plus_sym.
+Save.
+Hints Resolve mult_sym : arith v62.
+
+Lemma mult_n_1 : (n:nat)(mult n (S O))=n.
+Intro; Elim mult_sym; Auto with arith.
+Save.
+Hints Resolve mult_n_1 : arith v62.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
new file mode 100755
index 000000000..d57ec2d51
--- /dev/null
+++ b/theories/Arith/Peano_dec.v
@@ -0,0 +1,17 @@
+
+(* $Id$ *)
+
+Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
+Proof.
+Induction n.
+Auto.
+Intros p H; Left; Exists p; Auto.
+Qed.
+
+Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}.
+Proof.
+Induction n; Induction m; Auto.
+Intros q H'; Elim (H q); Auto.
+Qed.
+
+Hints Resolve O_or_S eq_nat_dec : arith.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
new file mode 100755
index 000000000..f1bc532aa
--- /dev/null
+++ b/theories/Arith/Plus.v
@@ -0,0 +1,113 @@
+
+(* $Id$ *)
+
+(**************************************************************************)
+(*                         Properties of addition                         *)
+(**************************************************************************)
+
+Require Le.
+Require Lt.
+
+Lemma plus_sym : (n,m:nat)((plus n m)=(plus m n)).
+Proof.
+Intros n m ; Elim n ; Simpl ; Auto with arith.
+Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith.
+Qed.
+Hints Immediate plus_sym : arith v62.
+
+Lemma plus_Snm_nSm : 
+  (n,m:nat)(plus (S n) m)=(plus n (S m)).
+Intros.
+Simpl.
+Rewrite -> (plus_sym n m).
+Rewrite -> (plus_sym n (S m)).
+Trivial with arith.
+Qed.
+
+Lemma simpl_plus_l : (n,m,p:nat)((plus n m)=(plus n p))->(m=p).
+Proof.
+Induction n ; Simpl ; Auto with arith.
+Qed.
+
+Lemma plus_assoc_l : (n,m,p:nat)((plus n (plus m p))=(plus (plus n m) p)).
+Proof.
+Intros n m p; Elim n; Simpl; Auto with arith.
+Qed.
+Hints Resolve plus_assoc_l : arith v62.
+
+Lemma plus_permute : (n,m,p:nat) ((plus n (plus m p))=(plus m (plus n p))).
+Proof. 
+Intros; Rewrite (plus_assoc_l m n p); Rewrite (plus_sym m n); Auto with arith.
+Qed.
+
+Lemma plus_assoc_r : (n,m,p:nat)((plus (plus n m) p)=(plus n (plus m p))).
+Proof.
+Auto with arith.
+Qed.
+Hints Resolve plus_assoc_r : arith v62.
+
+Lemma simpl_le_plus_l : (p,n,m:nat)(le (plus p n) (plus p m))->(le n m).
+Proof.
+Induction p; Simpl; Auto with arith.
+Qed.
+
+Lemma le_reg_l : (n,m,p:nat)(le n m)->(le (plus p n) (plus p m)).
+Proof.
+Induction p; Simpl; Auto with arith.
+Qed.
+Hints Resolve le_reg_l : arith v62.
+
+Lemma le_reg_r : (a,b,c:nat) (le a b)->(le (plus a c) (plus b c)).
+Proof.
+Induction 1 ; Simpl; Auto with arith.
+Qed.
+Hints Resolve le_reg_r : arith v62.
+
+Lemma le_plus_plus : 
+	(n,m,p,q:nat) (le n m)->(le p q)->(le (plus n p) (plus m q)).
+Proof.
+Intros n m p q H H0.
+Elim H; Simpl; Auto with arith.
+Qed.
+
+Lemma le_plus_l : (n,m:nat)(le n (plus n m)).
+Proof.
+Induction n; Simpl; Auto with arith.
+Qed.
+Hints Resolve le_plus_l : arith v62.
+
+Lemma le_plus_r : (n,m:nat)(le m (plus n m)).
+Proof.
+Intros n m; Elim n; Simpl; Auto with arith.
+Qed.
+Hints Resolve le_plus_r : arith v62.
+
+Theorem le_plus_trans : (n,m,p:nat)(le n m)->(le n (plus m p)).
+Proof.
+Intros; Apply le_trans with m; Auto with arith.
+Qed.
+Hints Resolve le_plus_trans : arith v62.
+
+Lemma simpl_lt_plus_l : (n,m,p:nat)(lt (plus p n) (plus p m))->(lt n m).
+Proof.
+Induction p; Simpl; Auto with arith.
+Qed.
+
+Lemma lt_reg_l : (n,m,p:nat)(lt n m)->(lt (plus p n) (plus p m)).
+Proof.
+Induction p; Simpl; Auto with arith.
+Qed.
+Hints Resolve lt_reg_l : arith v62.
+
+Lemma lt_reg_r : (n,m,p:nat)(lt n m) -> (lt (plus n p) (plus m p)).
+Proof.
+Intros n m p H ; Rewrite (plus_sym n p) ; Rewrite (plus_sym m p).
+Elim p; Auto with arith.
+Qed.
+Hints Resolve lt_reg_r : arith v62.
+
+Theorem lt_plus_trans : (n,m,p:nat)(lt n m)->(lt n (plus m p)).
+Proof.
+Intros; Apply lt_le_trans with m; Auto with arith.
+Qed.
+Hints Immediate lt_plus_trans : arith v62.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
new file mode 100755
index 000000000..225ebeff5
--- /dev/null
+++ b/theories/Arith/Wf_nat.v
@@ -0,0 +1,137 @@
+
+(* $Id$ *)
+
+(* Well-founded relations and natural numbers *)
+
+Require Lt.
+
+Chapter  Well_founded_Nat.
+
+Variable A : Set.
+
+Variable f : A -> nat.
+Definition ltof := [a,b:A](lt (f a) (f b)).
+Definition gtof := [a,b:A](gt (f b) (f a)).
+
+Theorem well_founded_ltof : (well_founded A ltof).
+Proof.
+Red.
+Cut (n:nat)(a:A)(lt (f a) n)->(Acc A ltof a).
+Intros H a;  Apply (H (S (f a))); Auto with arith.
+Induction n.
+Intros; Absurd (lt (f a) O); Auto with arith.
+Intros m Hm a ltSma.
+Apply Acc_intro.
+Unfold ltof; Intros b ltfafb.
+Apply Hm.
+Apply lt_le_trans with (f a); Auto with arith.
+Qed.
+
+Theorem  well_founded_gtof : (well_founded A 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 : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
+Proof.
+Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a).
+Intros H a;  Apply (H (S (f a))); Auto with arith.
+Induction n.
+Intros; Absurd (lt (f a) O); Auto with arith.
+Intros m Hm a ltSma.
+Apply F.
+Unfold ltof; Intros b ltfafb.
+Apply Hm.
+Apply lt_le_trans with (f a); Auto with arith.
+Qed. 
+
+Theorem induction_gtof1 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
+Proof induction_ltof1.
+
+Theorem induction_ltof2 
+   : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
+Proof (well_founded_induction A ltof well_founded_ltof).
+
+Theorem induction_gtof2 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
+Proof induction_ltof2.
+
+
+(* 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 : (x,y:A) (R x y) -> (lt (f x) (f y)).
+
+Theorem well_founded_lt_compat : (well_founded A R).
+Proof.
+Red.
+Cut (n:nat)(a:A)(lt (f a) n)->(Acc A R a).
+Intros H a; Apply (H (S (f a))); Auto with arith.
+Induction n.
+Intros; Absurd (lt (f a) O); Auto with arith.
+Intros m Hm a ltSma.
+Apply Acc_intro.
+Intros b ltfafb.
+Apply Hm.
+Apply lt_le_trans with (f a); Auto with arith.
+Save.
+
+End Well_founded_Nat.
+
+Lemma lt_wf : (well_founded nat lt).
+Proof (well_founded_ltof nat [m:nat]m).
+
+Lemma lt_wf_rec1 : (p:nat)(P:nat->Set)
+              ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
+Proof [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
+     (induction_ltof1 nat [m:nat]m P F p).
+
+Lemma lt_wf_rec : (p:nat)(P:nat->Set)
+              ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
+Proof [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
+     (induction_ltof2 nat [m:nat]m P F p).
+
+Lemma lt_wf_ind : (p:nat)(P:nat->Prop)
+              ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
+Intros; Elim (lt_wf p); Auto with arith.
+Save.
+
+Lemma gt_wf_rec : (p:nat)(P:nat->Set)
+              ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
+Proof lt_wf_rec.
+
+Lemma gt_wf_ind : (p:nat)(P:nat->Prop)
+              ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
+Proof lt_wf_ind.
+
+Lemma lt_wf_double_rec : 
+  (P:nat->nat->Set)
+  ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
+   -> (p,q:nat)(P p q).
+Intros P Hrec p; Pattern p; Apply lt_wf_rec.
+Intros; Pattern q; Apply lt_wf_rec; Auto with arith.
+Save.
+
+Lemma lt_wf_double_ind : 
+  (P:nat->nat->Prop)
+  ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
+   -> (p,q:nat)(P p q).
+Intros P Hrec p; Pattern p; Apply lt_wf_ind.
+Intros; Pattern q; Apply lt_wf_ind; Auto with arith.
+Save.
+
+Hints Resolve lt_wf : arith.
+Hints Resolve well_founded_lt_compat : arith.