proposition: Lemma r_of_pq_oprob_subproof (p q : {oprob R}) : (0 < Prob.p [r_of OProb.p p, OProb.p q] < 1)%O.
proof: Proof. rewrite r_of_pqE; apply/andP; split. rewrite divr_gt0////. exact/RltP/oprob_gt0. rewrite s_of_pqE//. have := OProb.O1 (((oprob_to_real p).~ * (oprob_to_real q).~).~)%:opr. by move/andP=> [] /=. apply/RltP. rewrite -RdivE'. rewrite ltR_pdivr_mulr ?mul1R; last by apply/(oprob_gt0). rewrite ltR_neqAle; split; last exact/RleP/ge_s_of. rewrite s_of_pqE; apply/eqP/ltR_eqF. rewrite onemM !onemK -!RplusE -RoppE -addRA. apply/ltR_addl. have := oprob_gt0 ((oprob_to_real p).~ * oprob_to_real q)%:opr. by rewrite /= onemE mulrBl mul1r -RminusE//. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)