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