diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 09:16:22 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 09:16:22 +0000 |
| commit | 13f4bb39888f3fde579f0bebfef2c74e6e598560 (patch) | |
| tree | d78ddc1d9a8d9cf398e3c8a7ed95ff2f080bb2e7 | |
| parent | a17f7ecc5e80fc471f330d673ba28a6cb06bcdc7 (diff) | |
Zpow_facts.Zmult_power: kills a useless hypothesis
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11098 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index b5b73c1ab..bf25de4d6 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -195,13 +195,13 @@ Proof. destruct b;trivial;unfold Zgt in z;discriminate z. Qed. -Theorem Zmult_power: forall p q r, 0 <= q -> 0 <= r -> +Theorem Zmult_power: forall p q r, 0 <= r -> (p*q)^r = p^r * q^r. Proof. - intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto. - intros r1 H3 H4 H5. + intros p q r H1; generalize H1; pattern r; apply natlike_ind; auto. + clear r H1; intros r H1 H2 H3. unfold Zsucc; rewrite Zpower_exp; auto with zarith. - rewrite H4; repeat rewrite Zpower_exp; auto with zarith; ring. + rewrite H2; repeat rewrite Zpower_exp; auto with zarith; ring. Qed. Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith. |