proposition: Lemma mixing_rule : P |= X _|_ [% Y, W] | Z /\ P |= Y _|_ W | Z -> P |= [% X, W] _|_ Y | Z.
proof: Proof. case=> ? ?. apply/symmetry/cinde_drv_2C/contraction; last by []. exact/symmetry/weak_union. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond