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