proposition: Lemma summable_fin (f : I -> R) : summable f.
proof: Proof. exists (\sum_(i : [fset i | i : I]) `|f (val i)|). move=> J; apply: (big_fset_subset (F := \`|_|)). by move=> x; rewrite normr_ge0. by move=> i _; apply/imfsetP; exists i. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology