diff options
| author | Cyril Cohen | 2020-10-30 18:51:49 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 18:51:49 +0100 |
| commit | 07a2bf3aaa85730616cdaf116ef727fedef3ca30 (patch) | |
| tree | b2295a16ba082ae4d9f651040c8966d639cf4609 /mathcomp/ssreflect | |
| parent | 1ec04efdcd1b00a6ae651551699c8b815a2a063f (diff) | |
| parent | 5f430f0d093c8b16a172ef686aa9d194e69f412c (diff) | |
Merge pull request #610 from pi8027/iter-lemmas
Add new lemmas iterM and iterX in ssrnat
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 9f17eb9..ec83c2a 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 minnMl : left_distributive muln minn. 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. + (* 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. |