diff options
| author | Kazuhiko Sakaguchi | 2020-10-31 04:29:48 +0900 |
|---|---|---|
| committer | GitHub | 2020-10-31 04:29:48 +0900 |
| commit | 71f000ff0761cac402074f14fa9fd65d1529fdd5 (patch) | |
| tree | 9a2defba9e61e3591640870da05930084e8f808f | |
| parent | 07a2bf3aaa85730616cdaf116ef727fedef3ca30 (diff) | |
| parent | 21c5e7090cd305bfdc54c9741a89bbf5cb4fd9fa (diff) | |
Merge pull request #625 from CohenCyril/hotfix_ssrnat
Fix ssrnat
| -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. *) |