proposition: Lemma variance : `V X = 5/9.
proof: Proof. rewrite VarE expected /Ex /X /sq_RV /comp_RV /=. rewrite 3!big_ord_recl big_ord0 /=. rewrite !ffunE /bump /=. rewrite !S_INR (_ : 0%:R = 0) //. by field. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssrnum) mathcomp(Rstruct) Reals_ext ssrR realType_ext fdist proba