proposition: Lemma lee_fsum_nneg_subset [T : choiceType] [A B : set T] [f : T -> \bar R] : finite_set A -> finite_set B -> {subset A <= B} -> {in [predD B & A], forall t : T, 0 <= f t}%E -> (\sum_(t \in A) f t <= \sum_(t \in B) f t)%E.
proof: Proof. move=> finA finB AB f0; rewrite !fsbig_finite//=; apply: lee_sum_nneg_subfset. by apply/fsubsetP; rewrite -fset_set_sub//; apply/subsetP. by move=> t; rewrite !inE !in_fset_set// => /f0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal