proposition: Lemma decomposition : P |= X _|_ [% Y, W] | Z -> P |= X _|_ Y | Z.
proof: Proof. move=> H a b c. transitivity (\sum_(d <- fin_img W) `Pr[ [% X, [% Y, W]] = (a, (b, d)) | Z = c]). rewrite -cpr_eq_set1. rewrite (creasoning_by_cases _ W); apply eq_bigr => /= d _. by rewrite setX1 cpr_eq_set1 cpr_eq_pairA. transitivity (\sum_(d <- fin_img W) `Pr[ X = a | Z = c] * `Pr[ [% Y, W] = (b, d) | Z = c]). by apply eq_bigr => d _; rewrite H. rewrite -big_distrr /=; congr (_ * _). rewrite -cpr_eq_set1 (creasoning_by_cases _ W); apply eq_bigr => d _. by rewrite setX1 cpr_eq_set1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond