proposition: Lemma sumsmxMr_gen P m n A (B : 'M[F]_(m, n)) : ((\sum_(i | P i) A i)%MS *m B :=: \sum_(i | P i) <<A i *m B>>)%MS.
proof: Proof. apply/eqmxP/andP; split; last first. by apply/sumsmx_subP=> i Pi; rewrite genmxE submxMr ?(sumsmx_sup i). have [u ->] := sub_sumsmxP _ _ _ (submx_refl (\sum_(i | P i) A i)%MS). by rewrite mulmx_suml summx_sub_sums // => i _; rewrite genmxE -mulmxA submxMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)