From 5f430f0d093c8b16a172ef686aa9d194e69f412c Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 10 Oct 2020 02:01:06 +0900
Subject: Add new lemmas iterM and iterX in ssrnat

---
 CHANGELOG_UNRELEASED.md     | 1 +
 mathcomp/ssreflect/ssrnat.v | 8 ++++++++
 2 files changed, 9 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 251beb6..6dd90d2 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -45,6 +45,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl`
 - in `ssrnat.v`, new lemma: `oddS`
 - in `ssrnat.v`, new lemmas: `subnA`, `addnBn`, `addnCAC`, `addnACl`
+- in `ssrnat.v`, new lemmas: `iterM`, `iterX`
 - in `finset.v`, new lemmas: `mem_imset_eq`, `mem_imset2_eq`.
   These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become availabe (cf. Renamed section)
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 8b88821..d5b33cb 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1126,6 +1126,10 @@ Proof. by case=> // m n1 n2; rewrite /minn (fun_if (muln _)) ltn_pmul2l. Qed.
 Lemma minn_mull : left_distributive muln minn.
 Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minn_mulr. 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.
+
 (* Exponentiation. *)
 
 Definition expn_rec m n := iterop n muln m 1.
@@ -1220,6 +1224,10 @@ Proof. by move=> e_gt0; rewrite !eqn_leq !leq_exp2r. Qed.
 Lemma expIn e : e > 0 -> injective (expn^~ e).
 Proof. by move=> e_gt1 m n /eqP; rewrite eqn_exp2r // => /eqP. Qed.
 
+Lemma iterX (T : Type) (n m : nat) (f : T -> T) :
+  iter (n ^ m) f =1 iter m (iter n) f.
+Proof. elim: m => //= m ihm x; rewrite expnS iterM; exact/eq_iter. Qed.
+
 (* Factorial. *)
 
 Fixpoint fact_rec n := if n is n'.+1 then n * fact_rec n' else 1.
-- 
cgit v1.2.3