proposition: Lemma iterX (T : Type) (n m : nat) (f : T -> T) : iter (n ^ m) f =1 iter m (iter n) f.
proof: Proof. elim: m => //= m ihm x; rewrite expnS iterM; exact/eq_iter. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring