proposition: Lemma esum_fset (F : set T) a : finite_set F -> (forall i, i \in F -> 0 <= a i) -> \esum_(i in F) a i = \sum_(i \in F) a i.
proof: Proof. move=> finF f0; apply/eqP; rewrite eq_le; apply/andP; split; last first. by apply ereal_sup_ub; exists F => //; exact: fsets_self. apply ub_ereal_sup => /= ? -[F' [finF' F'F] <-]. apply/lee_fsum_nneg_subset => //; first exact/subsetP. by move=> t; rewrite inE/= => /andP[_] /f0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun