From 13f4bb39888f3fde579f0bebfef2c74e6e598560 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 11 Jun 2008 09:16:22 +0000
Subject: 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
---
 theories/ZArith/Zpow_facts.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index b5b73c1ab1..bf25de4d61 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.
-- 
cgit v1.2.3