proposition: Lemma sub_sums_genmxP (F : fieldType) (I : finType) (P : pred I) (m n : nat) (A : 'M[F]_(m, n)) (B_ : I -> 'M_(m, n)) : reflect (exists u_ : I -> 'M_m, A = \sum_(i | P i) u_ i *m B_ i) (A <= \sum_(i | P i) <<B_ i>>)%MS.
proof: Proof. apply: (iffP idP); last first. by move=> [u_ ->]; rewrite summx_sub_sums // => i _; rewrite genmxE submxMl. move=> /sub_sumsmxP [u_ hA]. have Hu i : exists v, u_ i *m <<B_ i>>%MS = v *m B_ i. by apply/submxP; rewrite (submx_trans (submxMl _ _)) ?genmxE. exists (fun i => projT1 (sig_eqW (Hu i))); rewrite hA. by apply: eq_bigr => i /= P_i; case: sig_eqW. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)