proposition: Lemma iterM (T : Type) (n m : nat) (f : T -> T) : iter (n * m) f =1 iter n (iter m f).
proof: Proof. by move=> x; elim: n => //= n <-; rewrite mulSn iterD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring