proposition: Lemma p_nonneg : [forall a : 'I_3, (0 <= p a)%mcR].
proof: Proof. apply/forallP => a. rewrite /p ffunE. apply/all_tnthP: a => /=. rewrite !andb_idr => * //; apply/RleP; lra. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssrnum) mathcomp(Rstruct) Reals_ext ssrR realType_ext fdist proba