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. apply/eqP. do 3 rewrite big_ord_recl. rewrite big_ord0 addR0 /=. rewrite /f !ffunE /= ifT; last by I3_eq. rewrite ifF; last by I3_neq. rewrite ifT; last by I3_eq. rewrite ifF; last by I3_neq. rewrite ifF; last by I3_neq. rewrite ifT; last by I3_eq. by field. Qed.
imports: mathcomp(all_ssreflect ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext fdist proba