proposition: Lemma summable_condl (S : T -> R) (P : pred T) : summable S -> summable (fun x => (P x)%:R * S x).
proof: Proof. case/summable_seqP=> M ge0_M leM; apply/summable_seqP. exists M => //; move=> J /leM /(le_trans _); apply. apply/ler_sum=> x _; case: (P x); rewrite (mul1r, mul0r) //. by rewrite normr0 normr_ge0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology