diff options
| author | Cyril Cohen | 2020-10-30 19:09:28 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-10-30 19:09:28 +0100 |
| commit | 21c5e7090cd305bfdc54c9741a89bbf5cb4fd9fa (patch) | |
| tree | 9a2defba9e61e3591640870da05930084e8f808f /mathcomp | |
| parent | 07a2bf3aaa85730616cdaf116ef727fedef3ca30 (diff) | |
fix ssrnat
Diffstat (limited to 'mathcomp')
| -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. *) |