proposition: Lemma sumsmxS P n (A B : I -> 'M[F]_n) : (forall i, P i -> A i <= B i)%MS -> (\sum_(i | P i) A i <= \sum_(i | P i) B i)%MS.
proof: Proof. by move=> sAB; apply/sumsmx_subP=> i Pi; rewrite (sumsmx_sup i) ?sAB. 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)