proposition: Lemma gerfinseq_psum S (r : seq T) : uniq r -> summable S -> \sum_(j <- r) `|S j| <= psum S.
proof: Proof. move=> uq_r /gerfin_psum -/(_ [fset x in r]); by rewrite (big_seq_fset \`|S|). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology