proposition: Lemma jproduct_rule_cond E F G : \Pr_P [E `* F | G] = \Pr_(fdistA P) [E | F `* G] * \Pr_(fdist_proj23 P) [F | G].
proof: Proof. rewrite /jcPr; rewrite !mulRA; congr (_ * _); last by rewrite fdist_proj23_snd. rewrite -mulRA -/(fdist_proj23 _) -Pr_fdistA. case/boolP : (Pr (fdist_proj23 P) (F `* G) == 0) => H; last by rewrite mulVR ?mulR1. suff -> : Pr (fdistA P) (E `* (F `* G)) = 0 by rewrite mul0R. by rewrite Pr_fdistA; exact/Pr_fdist_proj23_domin/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