proposition: Lemma contraction : P |= X _|_ W | [% Z, Y] -> P |= X _|_ Y | Z -> P |= X _|_ [% Y, W] | Z.
proof: Proof. move=> H1 H2 a [b d] c. rewrite cpr_eq_product_rule. transitivity (`Pr[X = a | [% Y, Z] = (b, c)] * `Pr[[% Y, W] = (b, d) | Z = c]). rewrite -cpr_eq_pairAr [in X in X * _ = _]cpr_eq_pairCr -cpr_eq_pairAr. case/boolP : (`Pr[ [% W, [% Z, Y]] = (d, (c, b))] == 0) => [/eqP|] H0. rewrite [in X in _ * X = _ * X]cpr_eqE. by rewrite -pr_eq_pairA pr_eq_pairC -pr_eq_pairA H0 div0R !mulR0. by rewrite (cinde_alt _ H1) // cpr_eq_pairCr. case/boolP : (`Pr[ [% Y, Z] = (b, c) ] == 0) => [/eqP|] H0. - rewrite [X in _ * X = _ * X]cpr_eqE. by rewrite pr_eq_pairAC pr_eq_domin_RV2 ?div0R ?mulR0. - by rewrite (cinde_alt _ H2). Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond