proposition: Lemma sub_sums_genmxP P m n p (A : 'M_(m, p)) (B_ : I -> 'M_(n, p)) : reflect (exists u_ : I -> 'M_(m, n), A = \sum_(i | P i) u_ i *m B_ i) (A <= \sum_(i | P i) <<B_ i>>)%MS.
proof: Proof. apply: (iffP idP) => [| [u_ ->]]; last first. by apply: summx_sub_sums => i _; rewrite genmxE; apply: submxMl. have [b] := ubnP #|P|; elim: b => // b IHb in P A *. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. by exists (fun _ => 0); rewrite big_pred0. rewrite (cardD1x Pi) (bigD1 i) //= => /IHb{b IHb} /= IHi. rewrite (adds_eqmx (genmxE _) (eqmx_refl _)) => /sub_addsmxP[u ->]. have [u_ ->] := IHi _ (submxMl u.2 _). exists [eta u_ with i |-> u.1]; rewrite (bigD1 i Pi)/= eqxx; congr (_ + _). by apply: eq_bigr => j /andP[_ /negPf->]. 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)