proposition: Lemma lee_dsum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T) (f : T -> \bar^d R) : {subset A <= B} -> {in [predD B & A], forall t, P t -> f t <= 0} -> \sum_(t <- B | P t) f t <= \sum_(t <- A | P t) f t.
proof: Proof. move=> AB f0; rewrite !dual_sumeE leeN2. apply: lee_sum_nneg_subfset => [//|? ? ?]; rewrite oppe_ge0; exact: f0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed