proposition: Lemma commr_mmap1_M h m1 m2 : (forall i x, GRing.comm x (h i)) -> mmap1 h (m1 + m2) = (mmap1 h m1) * (mmap1 h m2).
proof: Proof. move=> comm; pose F (i : 'I_n) := (h i ^+ m1 i) * (h i ^+ m2 i). rewrite /mmap1 (eq_bigr F) => [|i _]; last first. by rewrite mnmDE exprD. rewrite {}/F; elim/big_rec3: _; first by rewrite mulr1. move=> i y1 y2 y3 _ ->; rewrite -!mulrA; congr (_ * _). have commn k j x: GRing.comm x ((h j)^+k) by apply/commrX. by rewrite -commn -mulrA commn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg