proposition: Lemma iter_combine {A : Type} (op : A -> A -> A) (e1 e2 : A) (assoc: associative op)(cm : op e1 e2 = op e2 e1) n m : op (iter n (op e1) e2) (iter m (op e1) e2) = (iter (n + m) (op e1) (op e2 e2)).
proof: Proof. elim: m n => [ | m Ih] n. rewrite addn0 /=. elim:n => [| n Ih] //=. by rewrite -assoc; congr op. by rewrite !iterS assoc -iter_comm // -iterS Ih addnS addSn. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)