proposition: Lemma jcPr_fdistA_AC (E : {set A}) (F : {set B}) (G : {set C}) : \Pr_(fdistA (fdistAC P))[E | G `* F] = \Pr_(fdistA P)[E | F `* G].
proof: Proof. rewrite /jcPr 2!Pr_fdistA Pr_fdistAC; congr (_ / _). by rewrite fdistA_AC_snd -Pr_fdistX fdistXI. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba