proposition: Lemma fst_RV2 : (`p_[% X, Y])`1 = `p_X.
proof: Proof. by rewrite /fdist_fst /dist_of_RV 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