proposition: Lemma summable_of_bd (S : T -> R) (d : R) : (forall J, uniq J -> \sum_(x <- J) `|S x| <= d) -> summable S /\ psum S <= d.
proof: Proof. move=> leS; have ge0_d: 0 <= d. by apply/(le_trans _ (leS [::] _)); rewrite // big_nil. have smS: summable S by apply/summable_seqP; exists d. split=> //; rewrite /psum (asboolT smS); apply/sup_le_ub. by exists 0, fset0; rewrite big_fset0. apply/ubP=> _ [J ->]; rewrite (big_fset_seq \`|_|) /=. by apply/leS; 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