proposition: Lemma expected : `E X = 5/3.
proof: Proof. rewrite /Ex. rewrite 3!big_ord_recl big_ord0 /=. rewrite /X !ffunE !(tnth_nth 0) /=. cbv; by field. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssrnum) mathcomp(Rstruct) Reals_ext ssrR realType_ext fdist proba