proposition: Lemma subset_pr A B mu : {subset B <= A} -> \P_[mu] B <= \P_[mu] A.
proof: Proof. move=> le_BA; apply/le_psum; last first. apply/summableMl => //; exists 1=> // x. by rewrite ger0_norm ?(ler0n, lern1) ?leq_b1. move=> x; rewrite mulr_ge0 ?ler0n ?ler_wpM2r //. rewrite ler_nat; have := le_BA x; rewrite -!topredE /=. by case: (B x) => // ->. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum