proposition: Lemma r_of_pq_is_r {R : realType} (p q r s : {prob R}) : r != 0%:pr -> s != 0%:pr -> (Prob.p p = Prob.p r * Prob.p s :> R -> (Prob.p s).~ = (Prob.p p).~ * (Prob.p q).~ -> [r_of p, q] = r)%mcR.
proof: Proof. move=> r0 s0 H1 H2; apply val_inj => /=. by rewrite r_of_pqE s_of_pqE -H2 onemK H1 -mulrA divff ?mulr1//. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)