diff options
Diffstat (limited to 'theories/ZArith/Zpow_alt.v')
| -rw-r--r-- | theories/ZArith/Zpow_alt.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v index a35dcb68..8f661a9c 100644 --- a/theories/ZArith/Zpow_alt.v +++ b/theories/ZArith/Zpow_alt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -30,12 +30,12 @@ Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope. Lemma Piter_mul_acc : forall f, (forall x y:Z, (f x)*y = f (x*y)) -> - forall p k, Pos.iter p f k = (Pos.iter p f 1)*k. + forall p k, Pos.iter f k p = (Pos.iter f 1 p)*k. Proof. intros f Hf. induction p; simpl; intros. - - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Hf, Z.mul_assoc. - - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Z.mul_assoc. + - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Hf, Z.mul_assoc. + - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Z.mul_assoc. - now rewrite Hf, Z.mul_1_l. Qed. |