From 9083a3af53765a2d7e0648b4d533cf1c4a4a8d6c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 28 Oct 2003 19:35:07 +0000
Subject: Simplification preuve

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4734 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/ZArithRing.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index 65fd1bc64a..cf5e18c5ea 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -21,10 +21,9 @@ Definition Zeq := [x,y:Z]
   end.
 
 Lemma Zeq_prop : (x,y:Z)(Is_true (Zeq x y)) -> x==y.
-  Intros x y; Unfold Zeq.
-  Generalize (let (H1,H2)=(Zcompare_EGAL x y) in H1).
-  Elim (Zcompare x y); [Intro; Rewrite H; Trivial | Contradiction | 
-	Contradiction ].
+  Intros x y H; Unfold Zeq in H.
+  Apply Zcompare_EGAL_eq.
+  NewDestruct (Zcompare x y); [Reflexivity | Contradiction | Contradiction ].
 Save.
 
 Definition ZTheory : (Ring_Theory Zplus Zmult `1` `0` Zopp Zeq).
-- 
cgit v1.2.3