proposition: Lemma iter_comm {A : Type} (op : A -> A -> A) (e1 e2 : A) (assoc: associative op)(cm : op e1 e2 = op e2 e1) n : op e1 (iter n (op e1) e2) = op (iter n (op e1) e2) e1.
proof: Proof. elim: n => [ | n Ih] //. by rewrite [in RHS]iterS -assoc -Ih -iterS. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)