proposition: Lemma prob_trichotomy p : p = 0%:pr \/ p = 1%:pr \/ 0 < Prob.p p < 1.
proof: Proof. have [/eqP ->|pneq0]:= boolP (p == 0%:pr); first by left. right. have [/eqP ->|pneq1] := boolP (p == 1%:pr); first by left. by right; apply/andP; split; [exact/prob_gt0|exact/prob_lt1]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)