proposition: Lemma jPr_Pr : \Pr_(`p_[% X, Y]) [E | F] = `Pr[X \in E |Y \in F].
proof: Proof. rewrite /jcPr Pr_fdistmap_RV2/= cpr_eq_setE /cPr; congr (_ / _). rewrite Pr_fdist_snd setTE Pr_fdistmap_RV2/=. rewrite (_ : [set x | X x \in [set: A]] = setT) ?setTI//. by apply/setP => x; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba