diff options
| author | herbelin | 2000-10-27 22:34:15 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-27 22:34:15 +0000 |
| commit | 7f1e3ede102a244ffcae8e6f15e999e0edbab8cb (patch) | |
| tree | 8d18e46bd6b74acffc71c7ba4ee3849bcb9e9ae0 | |
| parent | d4f8643a9f5aff3c0f819b4b7aafda4b782ef55d (diff) | |
Simpl fait trop maintenant; faut adapter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@778 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/omega/Zpower.v | 8 |
1 files 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. |