proposition: Lemma ger_big_psum r : uniq r -> summable S -> \sum_(x <- r) `|S x| <= psum S.
proof: Proof. move=> uq_r smS; rewrite /psum (asboolT smS). set E := (X in sup X). have : has_sup E by apply/summable_sup. move/sup_upper_bound/ubP; apply. by exists [fset x in r]; rewrite (big_seq_fset (fun i => `|S i|)). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology