proposition: Lemma E_comp_RV f k : (forall x y, f (x * y) = f x * f y) -> `E (f `o (k `cst* X)) = `E ((f k) `cst* (f `o X)).
proof: Proof. by move=> H; rewrite /comp_RV /=; apply eq_bigr => u _; rewrite 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