From 7f1e3ede102a244ffcae8e6f15e999e0edbab8cb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Oct 2000 22:34:15 +0000
Subject: Simpl fait trop maintenant; faut adapter

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@778 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/Zpower.v | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index c696aec28c..82eeb45737 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -126,12 +126,8 @@ Theorem shift_nat_correct :
 
 Unfold shift_nat; Induction n; 
 [ Simpl; Trivial with zarith
-| Intros; Simpl;
-Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`;
-[ Replace (POS (xO (iter_nat n0 positive xO x))) 
-  with `2 * (POS (iter_nat n0 positive xO x))`; 
-  [ Rewrite -> (H x); Apply Zmult_assoc    
-  | Auto with zarith ]
+| Intros; Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`;
+[ Rewrite <- Zmult_assoc; Rewrite <- (H x); Simpl; Reflexivity
 | Auto with zarith ]
 ].
 Save.
-- 
cgit v1.2.3