proposition: Lemma Pr_fdistmap (A B : finType) (f : A -> B) (d : real_realType.-fdist A) (E : {set A}) : injective f -> Pr d E = Pr (fdistmap f d) (f @: E).
proof: Proof. move=> bf; rewrite /Pr. under [in RHS]eq_bigr do rewrite fdistmapE. rewrite (exchange_big_dep (mem E)) /=; last first. by move=> _ a /imsetP[a' a'E ->]; rewrite 2!inE => /eqP /bf ->. apply eq_bigr => a aE; rewrite (big_pred1 (f a)) // => b /=. by rewrite !inE andb_idl //= => /eqP <-{b}; apply/imsetP; exists a. 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