proposition: Lemma p_of_rsE r s : Prob.p [p_of r, s] = (Prob.p r * Prob.p s)%mcR :> R.
proof: Proof. by rewrite /p_of_rs; unlock. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)