proposition: Lemma expected : `E X = 5/3.
proof: Proof. rewrite /Ex. rewrite 3!big_ord_recl big_ord0 /=. rewrite /pmf /X !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