proposition: Lemma sub_dsumsmx : mxdirect (\sum_(i | P i) B i) -> (A <= \sum_(i | P i) B i)%MS -> sub_dsumsmx_spec.
proof: Proof. move/mxdirect_sumsP=> dxB /sub_sumsmxP[u defA]. pose A_ i := u i *m B i. exists A_ => //= [i _ | C sCB defAC i Pi]; first exact: submxMl. apply/eqP; rewrite -subr_eq0 -submx0 -{dxB}(dxB i Pi) /=. rewrite sub_capmx addmx_sub ?eqmx_opp ?submxMl ?sCB //=. rewrite -(subrK A (C i)) -addrA -opprB addmx_sub ?eqmx_opp //. rewrite addrC defAC (bigD1 i) // addKr /= summx_sub // => j Pi'j. by rewrite (sumsmx_sup j) ?sCB //; case/andP: Pi'j. rewrite addrC defA (bigD1 i) // addKr /= summx_sub // => j Pi'j. by rewrite (sumsmx_sup j) ?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)