proposition: Lemma cpr_in_pairC E F G : `Pr[ [% Y, X] \in E `* F | Z \in G ] = `Pr[ [% X, Y] \in F `* E | Z \in G ].
proof: Proof. rewrite cpr_inE. rewrite pr_in_pairC pr_in_pairA pr_in_pairAC -pr_in_pairA pr_in_pairC. by rewrite -cpr_inE. 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