proposition: Lemma lee_sum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar R) : {subset Q <= P} -> {in [predD P & Q], forall i, 0 <= f i} -> \sum_(i <- s | Q i) f i <= \sum_(i <- s | P i) f i.
proof: Proof. move=> QP PQf; rewrite big_mkcond [leRHS]big_mkcond lee_sum// => i. by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed