Documentation/Structuration

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

6 files changed, 218 insertions, 169 deletions

diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index b730e9d7f..ce4661df6 100755
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -16,6 +16,8 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
+(** Order and successor *)
+
 Theorem gt_Sn_O : (n:nat)(gt (S n) O).
 Proof.
   Auto with arith.
@@ -28,63 +30,60 @@ Proof.
 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).
+Lemma gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n).
 Proof.
-  Red; Intros; Apply lt_le_trans with m; Auto with arith.
+  Auto with arith.
 Qed.
+Hints Immediate gt_S_n : arith v62.
 
-Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p).
+Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(m=n)).
 Proof.
-  Red; Intros; Apply lt_le_trans with m; Auto with arith.
+  Intros n m H; Unfold gt; Apply le_lt_or_eq; Auto with arith.
 Qed.
 
-Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p).
+Lemma gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n).
 Proof.
-  Red; Intros; Apply le_lt_trans with m; Auto with arith.
+  Auto with arith.
 Qed.
+Hints Immediate gt_pred : arith v62.
 
-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.
+(** Irreflexivity *)
 
 Lemma gt_antirefl : (n:nat)~(gt n n).
 Proof lt_n_n.
 Hints Resolve gt_antirefl : arith v62.
 
+(** Asymmetry *)
+
 Lemma gt_not_sym : (n,m:nat)(gt n m) -> ~(gt m n).
 Proof [n,m:nat](lt_not_sym m n).
 
+Hints Resolve gt_not_sym : arith v62.
+
+(** Relating strict and large orders *)
+
+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_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.
+Hints Resolve gt_not_le : arith v62.
 
-Lemma gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n).
+Theorem le_S_gt : (n,m:nat)(le (S n) m)->(gt m n).
 Proof.
   Auto with arith.
 Qed.
-Hints Immediate gt_S_n : arith v62.
+Hints Immediate le_S_gt : arith v62.
 
 Lemma gt_S_le : (n,p:nat)(gt (S p) n)->(le n p).
 Proof.
@@ -104,22 +103,40 @@ Proof.
 Qed.
 Hints Resolve le_gt_S : arith v62.
 
-Lemma gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n).
+(** Transitivity *)
+
+Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p).
 Proof.
-  Auto with arith.
+  Red; Intros; Apply lt_le_trans with m; 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)).
+Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p).
 Proof.
-  Intros n m H; Unfold gt; Apply le_lt_or_eq; Auto with arith.
+  Red; Intros; Apply le_lt_trans with m; Auto with arith.
+Qed.
+
+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.
+
+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 gt_O_eq : (n:nat)((gt n O)\/(<nat>O=n)).
+Hints Resolve gt_trans_S le_gt_trans gt_le_trans : arith v62.
+
+(** Comparison to 0 *)
+
+Theorem gt_O_eq : (n:nat)((gt n O)\/(O=n)).
 Proof.
   Intro n ; Apply gt_S ; Auto with arith.
 Qed.
 
+(** Simplification and compatibility *)
+
 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.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 92e56206b..c0a81d23e 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -14,15 +14,20 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
-Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
-Proof.
-  NewInduction 1; Auto.
-Qed.
+(** Transitivity *)
 
 Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p).
 Proof.
   NewInduction 2; Auto.
 Qed.
+Hints Immediate le_trans : arith v62.
+
+(** Order, successor and predecessor *)
+
+Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
+Proof.
+  NewInduction 1; Auto.
+Qed.
 
 Theorem le_n_Sn : (n:nat)(le n (S n)).
 Proof.
@@ -34,7 +39,7 @@ Proof.
   NewInduction n ; Auto.
 Qed.
 
-Hints Resolve le_n_S le_n_Sn le_O_n le_n_S le_trans : arith v62.
+Hints Resolve le_n_S le_n_Sn le_O_n le_n_S : arith v62.
 
 Theorem le_pred_n : (n:nat)(le (pred n) n).
 Proof.
@@ -44,18 +49,13 @@ 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.
+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.
@@ -67,51 +67,41 @@ NewDestruct m as [|m]. Simpl. Intro H. Inversion H.
 Simpl. Auto with arith.
 Qed.
 
-(** Negative properties *)
+(** Comparison to 0 *)
 
 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_n_O_eq : (n:nat)(le n O)->(O=n).
+Proof.
+NewInduction n; Auto with arith.
+Intro; Contradiction le_Sn_O with n.
+Qed.
+Hints Immediate le_n_O_eq : arith v62.
+
+(** Negative properties *)
+
 Theorem le_Sn_n : (n:nat)~(le (S n) n).
 Proof.
 NewInduction n; Auto with arith.
 Qed.
 Hints Resolve le_Sn_n : arith v62.
 
+(** Antisymmetry *)
+
 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.
+Intros n m h ; NewDestruct h as [|m0]; Auto with arith.
+Intros 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)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index beb32fac8..8c80e64c2 100755
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -14,6 +14,52 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
+(** Irreflexivity *)
+
+Theorem lt_n_n : (n:nat)~(lt n n).
+Proof le_Sn_n.
+Hints Resolve lt_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 le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
+Proof.
+NewInduction 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.
+
+(** Asymmetry *)
+
+Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
+Proof.
+NewInduction 1; Auto with arith.
+Qed.
+
+(** Order and successor *)
+
 Theorem lt_n_Sn : (n:nat)(lt n (S n)).
 Proof.
 Auto with arith.
@@ -48,11 +94,9 @@ 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.
+(** Predecessor *)
 
-Lemma S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))).
+Lemma S_pred : (n,m:nat)(lt m n)->n=(S (pred n)).
 Proof.
 NewInduction 1; Auto with arith.
 Qed.
@@ -68,45 +112,6 @@ NewDestruct 1; Simpl; Auto with arith.
 Qed.
 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.
-NewInduction 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.
-NewInduction 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).
@@ -126,30 +131,24 @@ 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.
-NewInduction 1; Auto with arith.
-Qed.
+(** Large = strict or equal *)
 
-Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
+Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
 Proof.
-Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith.
 NewInduction 1; Auto with arith.
 Qed.
 
-Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
+Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m).
 Proof.
-NewInduction 1; Auto with arith.
+Auto with arith.
 Qed.
+Hints Immediate lt_le_weak : arith v62.
 
-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.
+(** Dichotomy *)
 
-Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
+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.
 NewInduction 1; Auto with arith.
 Qed.
 
@@ -160,3 +159,18 @@ 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 : (n:nat)(~O=n)->(lt O n).
+Proof.
+NewInduction 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.
+NewInduction 1; Auto with arith.
+Qed.
+Hints Immediate lt_O_neq : arith v62.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 8224b8535..c8e9a5d40 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -18,12 +18,7 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
-Lemma minus_plus_simpl : 
-	(n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).
-Proof.
-  NewInduction p; Simpl; Auto with arith.
-Qed.
-Hints Resolve minus_plus_simpl : arith v62.
+(** 0 is right neutral *)
 
 Lemma minus_n_O : (n:nat)(n=(minus n O)).
 Proof.
@@ -31,12 +26,37 @@ NewInduction n; Simpl; Auto with arith.
 Qed.
 Hints Resolve minus_n_O : arith v62.
 
+(** Permutation with successor *)
+
+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.
+
+Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
+NewInduction x; Simpl; Auto with arith.
+Qed.
+
+(** Diagonal *)
+
 Lemma minus_n_n : (n:nat)(O=(minus n n)).
 Proof.
 NewInduction n; Simpl; Auto with arith.
 Qed.
 Hints Resolve minus_n_n : arith v62.
 
+(** Simplification *)
+
+Lemma minus_plus_simpl : 
+	(n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).
+Proof.
+  NewInduction p; Simpl; Auto with arith.
+Qed.
+Hints Resolve minus_plus_simpl : arith v62.
+
+(** Relation with plus *)
+
 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.
@@ -63,6 +83,8 @@ Symmetry; Auto with arith.
 Qed.
 Hints Resolve le_plus_minus_r : arith v62.
 
+(** Relation with order *)
+
 Theorem le_minus: (i,h:nat) (le (minus i h) i).
 Proof.
 Intros i h;Pattern i h; Apply nat_double_ind; [
@@ -71,13 +93,6 @@ Intros i h;Pattern i h; Apply nat_double_ind; [
 | Intros m n H; Simpl; Apply le_trans with m:=m; Auto ].
 Qed.
 
-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.
@@ -96,11 +111,6 @@ Intros; Absurd (lt O O); Trivial with arith.
 Qed.
 Hints Immediate lt_O_minus_lt : arith v62.
 
-Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
-NewInduction x; Auto with arith.
-Qed.
-
-
 Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O.
 Intros y x; Pattern y x ; Apply nat_double_ind; [
   Simpl; Trivial with arith
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 00a3b945a..99dc47942 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -18,7 +18,7 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
-(** Multiplication *)
+(** Distributivity *)
 
 Lemma mult_plus_distr : 
       (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))).
@@ -41,11 +41,7 @@ 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.
-NewInduction m; Simpl; Auto with arith.
-Qed.
-Hints Resolve mult_O_le : arith v62.
+(** Associativity *)
 
 Lemma mult_assoc_r : (n,m,p:nat)((mult (mult n m) p) = (mult n (mult m p))).
 Proof.
@@ -61,11 +57,7 @@ Auto with arith.
 Qed.
 Hints Resolve mult_assoc_l : arith v62.
 
-Lemma mult_1_n : (n:nat)(mult (S O) n)=n.
-Proof.
-Simpl; Auto with arith.
-Qed.
-Hints Resolve mult_1_n : arith v62.
+(** Commutativity *)
 
 Lemma mult_sym : (n,m:nat)(mult n m)=(mult m n).
 Proof.
@@ -75,12 +67,28 @@ Elim H; Apply plus_sym.
 Qed.
 Hints Resolve mult_sym : arith v62.
 
+(** 1 is neutral *)
+
+Lemma mult_1_n : (n:nat)(mult (S O) n)=n.
+Proof.
+Simpl; Auto with arith.
+Qed.
+Hints Resolve mult_1_n : arith v62.
+
 Lemma mult_n_1 : (n:nat)(mult n (S O))=n.
 Proof.
 Intro; Elim mult_sym; Auto with arith.
 Qed.
 Hints Resolve mult_n_1 : arith v62.
 
+(** Compatibility with orders *)
+
+Lemma mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)).
+Proof.
+NewInduction m; Simpl; Auto with arith.
+Qed.
+Hints Resolve mult_O_le : arith v62.
+
 Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)).
 Proof.
   NewInduction m. Intros. Simpl. Apply le_n.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 843ba0739..d73b9820d 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -18,6 +18,8 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p,q:nat.
 
+(** Commutativity *)
+
 Lemma plus_sym : (n,m:nat)(n+m)=(m+n).
 Proof.
 Intros n m ; Elim n ; Simpl ; Auto with arith.
@@ -25,6 +27,8 @@ Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith.
 Qed.
 Hints Immediate plus_sym : arith v62.
 
+(** Associativity *)
+
 Lemma plus_Snm_nSm : (n,m:nat)((S n)+m)=(n+(S m)).
 Intros.
 Simpl.
@@ -33,11 +37,6 @@ Rewrite -> (plus_sym n (S m)).
 Trivial with arith.
 Qed.
 
-Lemma simpl_plus_l : (n,m,p:nat)((n+m)=(n+p))->(m=p).
-Proof.
-NewInduction n ; Simpl ; Auto with arith.
-Qed.
-
 Lemma plus_assoc_l : (n,m,p:nat)((n+(m+p))=((n+m)+p)).
 Proof.
 Intros n m p; Elim n; Simpl; Auto with arith.
@@ -55,11 +54,25 @@ Auto with arith.
 Qed.
 Hints Resolve plus_assoc_r : arith v62.
 
+(** Simplification *)
+
+Lemma simpl_plus_l : (n,m,p:nat)((n+m)=(n+p))->(m=p).
+Proof.
+NewInduction n ; Simpl ; Auto with arith.
+Qed.
+
+(** Relations with order *)
+
 Lemma simpl_le_plus_l : (p,n,m:nat) (p+n)<=(p+m) -> n<=m.
 Proof.
 NewInduction p; Simpl; Auto with arith.
 Qed.
 
+Lemma simpl_lt_plus_l : (n,m,p:nat) (p+n)<(p+m) -> n<m.
+Proof.
+NewInduction p; Simpl; Auto with arith.
+Qed.
+
 Lemma le_reg_l : (n,m,p:nat) n<=m -> (p+n)<=(p+m).
 Proof.
 NewInduction p; Simpl; Auto with arith.
@@ -72,12 +85,6 @@ NewInduction 1 ; Simpl; Auto with arith.
 Qed.
 Hints Resolve le_reg_r : arith v62.
 
-Lemma le_plus_plus : (n,m,p,q:nat)  n<=m -> p<=q -> (n+p)<=(m+q).
-Proof.
-Intros n m p q H H0.
-Elim H; Simpl; Auto with arith.
-Qed.
-
 Lemma le_plus_l : (n,m:nat) n<=(n+m).
 Proof.
 NewInduction n; Simpl; Auto with arith.
@@ -96,10 +103,11 @@ Intros; Apply le_trans with m:=m; Auto with arith.
 Qed.
 Hints Resolve le_plus_trans : arith v62.
 
-Lemma simpl_lt_plus_l : (n,m,p:nat) (p+n)<(p+m) -> n<m.
+Theorem lt_plus_trans : (n,m,p:nat) n<m -> n<(m+p).
 Proof.
-NewInduction p; Simpl; Auto with arith.
+Intros; Apply lt_le_trans with m:=m; Auto with arith.
 Qed.
+Hints Immediate lt_plus_trans : arith v62.
 
 Lemma lt_reg_l : (n,m,p:nat) n<m -> (p+n)<(p+m).
 Proof.
@@ -114,11 +122,11 @@ Elim p; Auto with arith.
 Qed.
 Hints Resolve lt_reg_r : arith v62.
 
-Theorem lt_plus_trans : (n,m,p:nat) n<m -> n<(m+p).
+Lemma le_plus_plus : (n,m,p,q:nat)  n<=m -> p<=q -> (n+p)<=(m+q).
 Proof.
-Intros; Apply lt_le_trans with m:=m; Auto with arith.
+Intros n m p q H H0.
+Elim H; Simpl; Auto with arith.
 Qed.
-Hints Immediate lt_plus_trans : arith v62.
 
 Lemma le_lt_plus_plus : (n,m,p,q:nat)  n<=m -> p<q -> (n+p)<(m+q).
 Proof.
@@ -137,6 +145,7 @@ Proof.
   Apply lt_le_weak. Assumption.
 Qed.
 
+(** Inversion lemmas *)
 
 Lemma plus_is_O : (m,n:nat) (m+n)=O -> m=O /\ n=O.
 Proof.
@@ -153,6 +162,8 @@ Proof.
   Simpl in H. Discriminate H.
 Defined.
 
+(** Derived properties *)
+
 Lemma plus_permute_2_in_4 : (m,n,p,q:nat) ((m+n)+(p+q))=((m+p)+(n+q)).
 Proof.
   Intros. 
@@ -160,7 +171,6 @@ Proof.
   Rewrite (plus_sym n p). Rewrite <- (plus_assoc_l p n q). Apply plus_assoc_l.
 Qed.
 
-
 (** Tail-recursive plus *)
 
 (** [tail_plus] is an alternative definition for [plus] which is