proposition: Lemma psum_le S z : (forall J, uniq J -> \sum_(j <- J) `|S j| <= z) -> psum S <= z.
proof: Proof. move=> le_z; have: summable S; first (apply/summable_seqP; exists z). + by apply/(le_trans _ (le_z [::] _)) => //; rewrite big_nil. + by move=> J uqJ; apply/le_z. move/summable_sup=> [neS hsS]; rewrite psum_sup. apply/sup_le_ub => //; apply/ubP=> r [J ->]. by rewrite (big_fset_seq \`|_|) le_z /=; case: J => J /= /canonical_uniq. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology