proposition: Lemma lee_dsum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar^d 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 !dual_sumeE leeN2. apply: lee_sum_npos_subset => [//|i iPQ]; rewrite oppe_le0; exact: PQf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed