proposition: Lemma pq_is_rs {R : realType} (p q : {prob R}) : ((Prob.p p).~ * Prob.p q = (Prob.p [r_of p, q]).~ * Prob.p [s_of p, q])%R.
proof: Proof. case/boolP : (p == 0%:pr :> {prob R}) => p0. by rewrite (eqP p0) onem0 mul1r r_of_0q onem0 mul1r s_of_0q. rewrite r_of_pqE [in RHS]mulrBl mul1r -mulrA mulVf ?mulr1; last first. by rewrite prob_gt0; exact/s_of_gt0. rewrite s_of_pqE onemM !onemK /onem mulrBl mul1r [RHS]addrC !addrA. lra. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)