proposition: Lemma jcPr_fdistA_C12 (E : {set A}) (F : {set B}) (G : {set C}) : \Pr_(fdistA (fdistC12 P))[F | E `* G] = \Pr_(fdistA (fdistX (fdistA P)))[F | G `* E].
proof: Proof. rewrite /jcPr; congr (_ / _). by rewrite Pr_fdistA Pr_fdistC12 Pr_fdistA -[in RHS]Pr_fdistX fdistXI Pr_fdistA. rewrite -/(fdist_proj13 _) -(fdistXI (fdist_proj13 P)) -Pr_fdistX fdistXI; congr Pr. by rewrite /fdist_proj13 /fdistX /fdist_snd /fdistA !fdistmap_comp. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba