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