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