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 !(tnth_nth 0) /=. cbv; by field. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssrnum) mathcomp(Rstruct) Reals_ext ssrR realType_ext fdist proba