proposition: Lemma jcPr_fdistX_prod (A B : finType) (P : {fdist A}) (W : A -> {fdist B}) a b : P a <> 0 -> \Pr_(fdistX (P `X W))[ [set b] | [set a] ] = W a b.
proof: Proof. move=> Pxa. rewrite /jcPr setX1 fdistX2 2!Pr_set1 fdistXE fdist_prod1. by rewrite fdist_prodE /= /Rdiv mulRAC mulRV ?mul1R //; exact/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba