proposition: Lemma p_is_rs {R : realType} (p q : {prob R}) : Prob.p p = ((Prob.p [r_of p, q]) * Prob.p [s_of p, q])%R :> R.
proof: Proof. case/boolP : (p == 0%:pr :> {prob R}) => p0; first by rewrite (eqP p0) r_of_0q mul0r. case/boolP : (q == 0%:pr :> {prob R}) => q0. by rewrite (eqP q0) s_of_p0 r_of_p0 // mul1r. rewrite r_of_pqE -mulrA mulVf ?mulr1 //. suff : Prob.p [s_of p, q] != 0%R :> R by []. by rewrite prob_gt0 s_of_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)