proposition: Lemma prob_trichotomy' (p : {prob R}) (P : {prob R} -> Prop) : P prob0 -> P prob1 -> (forall o : {oprob R}, P (OProb.p o)) -> P p.
proof: Proof. move=> p0 p1 po. have [-> //|[->//|p01]] := prob_trichotomy p. apply (po (@OProb.mk _ _ p01)). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)