proposition: Lemma p_of_neq1 r s : (0 < Prob.p s < 1)%mcR -> [p_of r, s] != 1%:pr.
proof: Proof. case/andP=> p0 p1; apply/eqP => pq1; move: (p1). rewrite [X in (_ < X)%mcR -> _](_ : _ = Prob.p 1%:pr) //. rewrite -pq1 p_of_rsE -ltr_pdivrMr // divff ?gt_eqF//. by rewrite ltNge prob_le1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)