proposition: Lemma cpr_eqE (U : finType) (P : {fdist U}) (TA TB : eqType) (X : {RV P -> TA}) (Y : {RV P -> TB}) a b : `Pr[ X = a | Y = b ] = `Pr[ [% X, Y] = (a, b) ] / `Pr[Y = b].
proof: Proof. rewrite cpr_eqE' /cPr /dist_of_RV 2!pr_eqE; congr (Pr _ _ / _). by apply/setP => u; rewrite !inE xpair_eqE. 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