proposition: Lemma cpr_in_pairACr E F G H : `Pr[ X \in E | [% Y, Z, W] \in F `* G `* H ] = `Pr[ X \in E | [% Y, W, Z] \in F `* H `* G ].
proof: Proof. rewrite 2!cpr_inE; congr (_ / _). rewrite !pr_inE' !Pr_fdistmap_RV2; congr Pr. by apply/setP => u; rewrite !inE /= !andbA /= andbAC. by rewrite pr_in_pairAC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist