proposition: Lemma cpr_inE (U : finType) (P : {fdist U}) (A B : finType) (X : {RV P -> A}) (Z : {RV P -> B}) E F : `Pr[X \in E | Z \in F] = `Pr[ [%X, Z] \in E `* F] / `Pr[Z \in F].
proof: Proof. rewrite /cpr_eq_set; unlock. rewrite !pr_eq_setE /cPr; congr (Pr _ _ * _). by 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