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