proposition: Lemma oprob_mulR_subproof (p q : {oprob R}) : (0 < Prob.p (OProb.p p) * Prob.p (OProb.p q) < 1)%O.
proof: Proof. apply/andP; split. by rewrite mulr_gt0//; apply/RltP/oprob_gt0. by rewrite mulr_ilt1//; apply/RltP/oprob_lt1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)