proposition: Lemma psum_absE S : summable S -> psum S = sup [set x | exists J : {fset T}, x = \sum_(j : J) `|S (val j)|]%classic.
proof: Proof. by move=> smS; rewrite /psum (asboolT smS). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology