proposition: Lemma prob_trichotomy' (p : {prob R}) (P : {prob R} -> Prop) : P 0%:pr -> P 1%:pr -> (forall o : {oprob R}, P o) -> P p.
proof: Proof. move=> p0 p1 po. have [-> //|[->//| p01]] := prob_trichotomy p. exact (po (OProb.mk p01)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)