proposition: Lemma cinde_drv_2C : P |= X _|_ [% Y, W] | Z -> P |= X _|_ [% W, Y] | Z.
proof: Proof. move=> H a -[d b] c. by rewrite cpr_eq_pairA cpr_eq_pairAC -cpr_eq_pairA H cpr_eq_pairC. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond