proposition: Lemma lee_dsum_npos (I : eqType) (s : seq I) (P Q : pred I) (f : I -> \bar^d R) : (forall i, P i -> ~~ Q i -> f i <= 0) -> \sum_(i <- s | P i) f i <= \sum_(i <- s | P i && Q i) f i.
proof: Proof. move=> PQf; rewrite !dual_sumeE leeN2. apply: lee_sum_nneg => i Pi nQi; rewrite oppe_ge0; exact: PQf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed