L'exemple phare de modules - simplifie pour TPHOLs

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

1 files changed, 7 insertions, 56 deletions

diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index d0ad6a5e2..d3e98ae4d 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -6,63 +6,14 @@ Hints Unfold le.
 
 Lemma le_refl:(n:nat)(le n n).
   Auto.
-Save.
+Qed.
 
-Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
-  Unfold le.
-  Intros.
-  Generalize H.
-  Clear H.
-  Elim H0.
-  Auto.
-  Auto.  
-Save.
-
-Lemma le_mono_S : (n,m:nat)(le n m) -> (le (S n) (S m)).
-  Unfold le.
-  NewInduction 1.
-  Auto.
-  Auto.
-Save.
-
-Hints Resolve le_mono_S.
-
-Lemma le_pred_mono : (n,m:nat) (le n m) -> (le (pred n) (pred m)).
-  Unfold le.
-  Induction 1.
-  Auto.
-  Intro.
-  Case m0.
-  Auto.
-  Intro.
-  Simpl.
-  Auto.
-Save.
+Require Le.
 
-Hints Resolve le_pred_mono.  
-
-Lemma le_S_mono : (m,n:nat)(le (S n) (S m)) -> (le n m).
-  Intros.
-  Change (le (pred (S n)) (pred (S m))).
-  Auto.
-Save.
-
-Hints Resolve le_S_mono.
+Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
+  EAuto with arith.
+Qed.
 
 Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
-  NewInduction n.
-  Intros.
-  Inversion H0.
-  Reflexivity.
-
-  Intros.
-  Inversion H.
-  Auto.
-  Rewrite (IHn m0).
-  Auto.
-  Rewrite <- H2 in H.
-  Auto.
-  Rewrite <- H2 in H0.
-  Auto.
-Save.
-
+  EAuto with arith.
+Qed.