proposition: Lemma psum_sup S : psum S = sup [set x | exists J : {fset T}, x = \sum_(x : J) `|S (val x)|]%classic.
proof: Proof. rewrite /psum; case: ifPn => // /asboolPn h. rewrite sup_out //; set X := [set r | _]%classic => hs. apply: h; exists (sup X) => J. by move/ubP : (sup_upper_bound hs); 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