proposition: Lemma le_mu_pr A mu nu : (forall x, x \in dinsupp nu -> x \in A -> nu x <= mu x) -> \P_[nu] A <= \P_[mu] A.
proof: Proof. move=> h; apply/le_psum; last by apply/summable_pr. move=> x; rewrite mulr_ge0 ?ler0n //=. case/boolP: (x \in dinsupp nu) => [/h {}h|]; last first. by move/dinsuppPn=> ->; rewrite mulr0 mulr_ge0 ?ler0n. by case/boolP: (A x) => [/h|]; rewrite ?(mul0r, mul1r). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum