proposition: Lemma ler_suml [P Q : pred I] [F G : I -> R] : (forall i : I, P i -> F i <= G i) -> (forall i : I, Q i -> ~~ P i -> 0 <= G i) -> (forall i : I, P i -> Q i) -> \sum_(i <- r | P i) F i <= \sum_(i <- r | Q i) G i.
proof: Proof. move=> PFG QG0 PQ. move: PFG => /ler_sum /le_trans; apply. rewrite [leRHS](bigID P) /=. move: PQ => /(_ _) /andb_idl => /(eq_bigl _ G) ->. rewrite lerDl; apply: sumr_ge0=> i. by case/andP; exact: QG0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext