proposition: Lemma summx_sub_sums P m n (A : I -> 'M[F]_(m, n)) B : (forall i, P i -> A i <= B i)%MS -> ((\sum_(i | P i) A i)%R <= \sum_(i | P i) B i)%MS.
proof: Proof. by move=> sAB; apply: summx_sub => 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)