proposition: Lemma pr_dmargin E f (mu : {distr U / R}) : \P_[dmargin f mu] E = \P_[mu] [pred x | f x \in E].
proof: Proof. by rewrite /dmargin __deprecated__pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum