proposition: Lemma jproduct_rule E F : Pr P (E `* F) = \Pr_P[E | F] * Pr (P`2) F.
proof: Proof. have [/eqP PF0|PF0] := boolP (Pr (P`2) F == 0). rewrite jcPrE /cPr -{1}(setIT E) -{1}(setIT F) -setIX. rewrite Pr_domin_setI; last by rewrite -Pr_fdistX Pr_domin_setX // fdistX1. by rewrite setIC Pr_domin_setI ?(div0R,mul0R) // setTE Pr_setTX. rewrite -{1}(setIT E) -{1}(setIT F) -setIX product_rule. rewrite -EsetT setTT cPrET Pr_setT mulR1 jcPrE. rewrite /cPr {1}setTE {1}EsetT. by rewrite setIX setTI setIT setTE Pr_setTX -mulRA mulVR ?mulR1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba