proposition: Lemma variance : `V X = 5/9.
proof: Proof. rewrite VarE. rewrite expected. rewrite /Ex /X. do 3 rewrite big_ord_recl. rewrite big_ord0 addR0 /=. rewrite /sq_RV /comp_RV /=. rewrite !mul1R. rewrite {1}/pmf !ffunE /=. rewrite ifT; last by I3_eq. rewrite (_ : INR _ = 2) // mulR1. rewrite /f /=. rewrite ifF; last by I3_neq. rewrite ifT; last by I3_eq. rewrite (_ : INR _ = 3); last first. rewrite S_INR (_ : INR _ = 2) //; by field. rewrite ifF; last by I3_neq. rewrite ifF; last by I3_neq. rewrite ifT; last by I3_eq. field. Qed.
imports: mathcomp(all_ssreflect ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext fdist proba