proposition: Lemma summableZ (S : T -> R) c : summable S -> summable (c \*o S).
proof: Proof. case=> [M h]; exists (`|c| * M) => J; move/(_ J): h => /=. move/(ler_wpM2l (normr_ge0 c)); rewrite mulr_sumr. move/(le_trans _); apply; rewrite le_eqVlt; apply/orP. by left; apply/eqP/eq_bigr=> j _; rewrite normrM. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology