proposition: Lemma lee_fsum [T : choiceType] (I : set T) (a b : T -> \bar R) : finite_set I -> (forall i, I i -> a i <= b i)%E -> (\sum_(i \in I) a i <= \sum_(i \in I) b i)%E.
proof: Proof. move=> finI ab. rewrite !fsbig_finite// big_seq [in leRHS]big_seq lee_sum //. by move=> i; rewrite in_fset_set// inE; exact: ab. 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