proposition: Lemma summable_seqP S : summable S <-> (exists2 M, 0 <= M & forall s : seq T, uniq s -> \sum_(x <- s) `|S x| <= M).
proof: Proof. split=> [/summableP|] [M gt0_M h]; exists M => //. by move=> s uq_s; have := h [fset x in s]; rewrite (big_seq_fset \`|S|). by case=> J cJ; rewrite (big_fset_seq \`|_|) /=; apply/h/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