proposition: Lemma expected : `E X = 5/3.
proof: Proof. rewrite /Ex. do 3 rewrite big_ord_recl. rewrite big_ord0 addR0. rewrite /X mul1R. rewrite /f !ffunE /= ifT; last by I3_eq. rewrite (_ : INR _ = 2) //. 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 /f /= 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