proposition: Lemma Pr_fdistmap_RV2 (U : finType) (P : real_realType.-fdist U) (A B : finType) (E : {set A}) (F : {set B}) (X : {RV P -> A}) (Z : {RV P -> B}) : Pr `p_[% X, Z] (E `* F) = Pr P ([set x | preim X (mem E) x] :&: [set x | preim Z (mem F) x]).
proof: Proof. rewrite /Pr. transitivity (\sum_(a in ([% X, Z] @^-1: (E `* F))) P a); last first. by apply eq_bigl => u; rewrite !inE. rewrite [in RHS]partition_big_preimset /=. apply eq_big => // -[a c]; rewrite inE => /andP[/= aE cF]. by rewrite fdistmapE. 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