proposition: Lemma cpr_eq_set1 X x (Y : {RV P -> B}) y : `Pr[ X \in [set x] | Y \in [set y] ] = `Pr[ X = x | Y = y ].
proof: Proof. by rewrite cpr_eq_setE cpr_eqE'; congr cPr; apply/setP => u; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist