proposition: Lemma pmf_ge0 : [forall a : 'I_3, 0 <= pmf a].
proof: Proof. apply/forallPP; first by move=> x; exact/RleP. case/I3P. - rewrite /f ffunE /= eqxx; lra. - rewrite /f ffunE /= ifF; last by I3_neq. rewrite eqxx; lra. - rewrite /f ffunE /= ifF; last by I3_neq. rewrite ifF; last by I3_neq. rewrite eqxx; lra. Qed.
imports: mathcomp(all_ssreflect ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext fdist proba