proposition: Lemma q_of_rs_prob {R : realType} (r s : {prob R}) : (0 <= ((Prob.p r).~ * (Prob.p s)) / (Prob.p [p_of r, s]).~ <= 1)%R.
proof: Proof. case/boolP : (r == 1%:pr :> {prob R}) => r1. by rewrite (eqP r1) onem1 !mul0r lexx ler01. case/boolP : (s == 1%:pr :> {prob R}) => s1. rewrite (eqP s1) mulr1 p_of_r1 divff ?onem_neq0//. by rewrite ler01// lexx. apply/andP; split. by rewrite divr_ge0// mulr_ge0. rewrite ler_pdivrMr// ?mul1r; last first. rewrite onem_gt0// -prob_lt1. apply/p_of_rs1P/not_andP; left. exact/eqP. by rewrite p_of_rsE {2}/onem lerBrDr -mulrDl addrC onemKC mul1r. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)