proposition: Lemma cpr_in_pairAC E F G H : `Pr[ [% X, Y, Z] \in (E `* F `* G) | W \in H] = `Pr[ [% X, Z, Y] \in (E `* G `* F) | W \in H].
proof: Proof. rewrite 2!cpr_inE; congr (_ / _). rewrite !pr_inE' !Pr_fdistmap_RV2; congr Pr. apply/setP => u; rewrite !inE /=; congr (_ && _). by rewrite andbAC. 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