proposition: Lemma r_of_pqK {R : realType} (r s : {prob R}) : [p_of r, s] != 1%:pr -> s != 0%:pr -> [r_of [p_of r, s], [q_of r, s]] = r.
proof: Proof. move=> H1 s0; apply/val_inj => /=. rewrite !(r_of_pqE,s_of_pqE,q_of_rsE,p_of_rsE) /onem. field. apply/andP; split; last first. by rewrite mulrBl mul1r !opprB -!addrA addrC !addrA !subrK. rewrite subr_eq0. apply: contra H1 => /eqP H1. by apply/eqP/val_inj; rewrite /= p_of_rsE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)