diff options
Diffstat (limited to 'contrib/omega/Zpower.v')
| -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. |