Documentation/Structuration

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

1 files changed, 28 insertions, 18 deletions

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