proposition: Lemma le_in_pr E1 E2 mu : (forall x, x \in dinsupp mu -> x \in E1 -> x \in E2) -> \P_[mu] E1 <= \P_[mu] E2.
proof: Proof. move=> le; rewrite /pr; apply/le_psum; last by apply/summable_pr. move=> x; rewrite mulr_ge0 ?ler0n //=; case/boolP: (x \in dinsupp mu). move/le; rewrite -!topredE /= => E12; rewrite ler_wpM2r //. by rewrite ler_nat; case: (E1 x) E12 => // ->. by move/dinsuppPn=> ->; rewrite !mulr0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum