proposition: Lemma summableE D f : summable D f = (\esum_(x in D) `| f x | \is a fin_num).
proof: Proof. rewrite /summable fin_numElt; apply/idP/idP => [->|/andP[]//]. by rewrite andbT (lt_le_trans (ltNyr 0))//; exact: esum_ge0. 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