diff options
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index ec83c2a..ce7407d 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1128,7 +1128,7 @@ Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minnMr. Qed. Lemma iterM (T : Type) (n m : nat) (f : T -> T) : iter (n * m) f =1 iter n (iter m f). -Proof. by move=> x; elim: n => //= n <-; rewrite mulSn iter_add. Qed. +Proof. by move=> x; elim: n => //= n <-; rewrite mulSn iterD. Qed. (* Exponentiation. *) |