proposition: Lemma summableMl (S1 S2 : T -> R) : (exists M, forall x, `|S1 x| <= M) -> summable S2 -> summable (S1 \* S2).
proof: Proof. case=> M leM smS2; apply/summable_abs. apply/(le_summable (F2 := M \*o \`|S2|)). + by move=> x /=; rewrite normr_ge0 /= normrM ler_wpM2r. + by apply/summableZ/summable_abs. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology