proposition: Lemma E_comp_RV_ext f : X = Y -> `E (f `o X) = `E (f `o Y).
proof: Proof. move=> H; by rewrite /comp_RV /= H. 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