proposition: Lemma cpr_eq_product_rule (U : finType) (P : {fdist U}) (A B C : eqType) (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) a b c : `Pr[ [% X, Y] = (a, b) | Z = c ] = `Pr[ X = a | [% Y, Z] = (b, c) ] * `Pr[ Y = b | Z = c ].
proof: Proof. rewrite cpr_eqE'. rewrite (_ : [set x | preim [% X, Y] (pred1 (a, b)) x] = finset (X @^-1 a) :&: finset (Y @^-1 b)); last first. by apply/setP => u; rewrite !inE xpair_eqE. rewrite product_rule_cond cpr_eqE'; congr (cPr _ _ _ * _). - by apply/setP=> u; rewrite !inE xpair_eqE. - by rewrite cpr_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