proposition: Lemma summableP : summable -> { M | 0 <= M & forall (J : {fset T}), \sum_(x : J) `|f (val x)| <= M }.
proof: Proof. move/asboolP/exists_asboolP=> h; have := (xchooseP h). move: (xchoose _)=> {h} M /asboolP h; exists M => //. by have := h fset0; rewrite big_pred0 // => -[x]; rewrite in_fset0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology