proposition: Lemma s_of_pq_oprob_subproof (p q : {oprob R}) : (0 < Prob.p [s_of p, q] < 1)%O.
proof: Proof. rewrite s_of_pqE; apply/andP; split. - rewrite onem_gt0//= mulr_ilt1 ?onem_ge0 ?onem_lt1//. by have /andP[] := OProb.O1 p. by have /andP[] := OProb.O1 q. - rewrite onem_lt1// mulr_gt0// onem_gt0//. by have /andP[] := OProb.O1 p. by have /andP[] := OProb.O1 q. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)