proposition: Lemma Var_average n (X : {RV (P `^ n) -> R}) Xs (sum_Xs : X \=sum Xs) : forall sigma2, (forall i, `V (Xs ``_ i) = sigma2) -> n%:R * `V (X `/ n) = sigma2.
proof: Proof. move=> s Hs; destruct n; first by inversion sum_Xs. by rewrite (Var_scale X) // (V_sum_n sum_Xs Hs) //; field; exact/INR_eq0. 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