proposition: Lemma le_psum_condr (S : T -> R) (P : pred T) : summable S -> psum (fun x => S x * (P x)%:R) <= psum S.
proof: Proof. move=> smS; apply/(le_trans _ (le_psum_condl P smS)). rewrite le_eqVlt -(rwP orP); left; apply/eqP/eq_psum. 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