proposition: Lemma VarE : Var = `E (X `^2) - (`E X) ^ 2.
proof: Proof. rewrite /Var E_trans_RV_id_rem E_trans_add_RV E_sub_RV E_scalel_RV; field. 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