proposition: Lemma jfdist_cond_prod (A B : finType) (P : {fdist A}) (W : A -> {fdist B}) (a : A) : (P `X W)`1 a != 0 -> W a = (P `X W) `(| a ).
proof: Proof. move=> a0; apply/fdist_ext => b. rewrite jfdist_condE // /jcPr setX1 !Pr_set1 fdistXE fdistX2 fdist_prod1. rewrite fdist_prodE /= /Rdiv mulRAC mulRV ?mul1R //. by move: a0; rewrite fdist_prod1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba