proposition: Lemma pr_in_comp (f : A -> B) E : injective f -> `Pr[ X \in E ] = `Pr[ (f `o X) \in f @: E ].
proof: Proof. by move=> inj_f; rewrite 2!pr_inE' (Pr_fdistmap inj_f) fdistmap_comp. 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