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