proposition: Lemma summable_condr (S : T -> R) (P : pred T) : summable S -> summable (fun x => S x * (P x)%:R).
proof: Proof. move=> /(summable_condl P) /eq_summable; apply. by move=> x /=; rewrite mulrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology