proposition: Lemma RV_equivC (A B : eqType) (X : {RV P -> A}) (Y : {RV P -> B}) : RV_equiv X Y -> RV_equiv Y X.
proof: Proof. case=> -[f g] []/= cfg cgf Hf. exists (g,f) => //. move=> u /=. move/(f_equal g): (Hf u). by rewrite cfg. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba