diff options
| -rw-r--r-- | theories/ZArith/Zpow_def.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 8609a6af98..d4f58c3b04 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -25,9 +25,9 @@ Notation Zpower_Ppow := Pos2Z.inj_pow (only parsing). Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow. Proof. - constructor. intros. - destruct n;simpl;trivial. + constructor. intros z n. + destruct n as [|p];simpl;trivial. unfold Z.pow_pos. rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1. - induction p; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. + induction p as [p IHp|p IHp|]; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. Qed. |