proposition: Lemma iter_mul (n : nat) (m v : 'M[R]_2) : iter n [eta *%R m] v = m ^+ n * v.
proof: Proof. elim: n => [ | n Ih]. by rewrite /= expr0 mul1r. by rewrite /= Ih mulrA exprS. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)