proposition: Lemma pmf01 : [forall a, 0 <= pmf a] && (\sum_(a in 'I_3) pmf a == 1).
proof: Proof. apply/andP; split; first exact: pmf_ge0. by apply/eqP; rewrite 3!big_ord_recl big_ord0 /= /pmf !ffunE /=; field. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssrnum) mathcomp(Rstruct) Reals_ext ssrR realType_ext fdist proba