proposition: Lemma lee_sum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T) (f : T -> \bar 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 big_mkcond (big_fsetID _ (mem A) B) /=. rewrite -[leRHS]adde0 leeD //. rewrite -big_mkcond /= {3}(_ : A = [fset x in B | x \in A]%fset) //. by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB. rewrite big_fset /= big_seq_cond sume_le0 // => t /andP[tB tA]. by case: ifPn => // Pt; rewrite f0 // !inE tA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed