proposition: Lemma summableM (S1 S2 : T -> R) : summable S1 -> summable S2 -> summable (S1 \* S2).
proof: Proof. move=> smS1 smS2; apply/summableMl => //; exists (psum S1). by move=> x; apply/ger1_psum. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology