proposition: Lemma gerfin_psum S (J : {fset T}) : summable S -> \sum_(j : J) `|S (val j)| <= psum S.
proof: Proof. move=> smS; rewrite /psum (asboolT smS). by move/ubP : (sup_upper_bound (summable_sup smS)); apply; exists J. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology