proposition: Lemma prob_lt1 p : p != 1%:pr <-> Prob.p p < 1.
proof: Proof. rewrite lt_neqAle; split=> [H|/andP[+ pge0]]. by apply/andP; split => //; exact: prob_le1. by apply: contra => /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)