proposition: Lemma esum_set0 a : \esum_(i in set0) a i = 0.
proof: Proof. rewrite /esum fsets0 [X in ereal_sup X](_ : _ = [set 0%E]) ?ereal_sup1//. apply/seteqP; split=> [x [_ /= ->]|x]; first by rewrite fsbig_set0. by move=> -> /=; exists set0 => //; rewrite fsbig_set0. 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