proposition: Lemma r_of_pq_subproof {R : realType} (p q : {prob R}) : (0 <= Prob.p p / Prob.p [s_of p, q] <= 1)%R.
proof: Proof. have [->|p0] := eqVneq p 0%:pr. by rewrite mul0r lexx ler01. have [->|a0] := eqVneq q 0%:pr. by rewrite s_of_p0 divff// lexx ler01. apply/andP; split. - by rewrite divr_ge0. rewrite ler_pdivrMr ?mul1r. by apply: ge_s_of. by rewrite s_of_gt0//. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)