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