Documentation/Structuration

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

1 files changed, 48 insertions, 31 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.