proposition: Lemma pmf_ge0 : [forall a : 'I_3, (0 <= pmf a)%mcR].
proof: Proof. apply/forallP => a. rewrite /pmf ffunE /=. apply/RleP. do! case: ifP => _; lra. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssrnum) mathcomp(Rstruct) Reals_ext ssrR realType_ext fdist proba