proposition: Lemma s_of_pqK {R : realType} (r s : {prob R}) : [p_of r, s] != 1%:pr -> [s_of [p_of r, s], [q_of r, s]] = s.
proof: Proof. move=> H. apply/val_inj; rewrite /= s_of_pqE p_of_rsE q_of_rsE p_of_rsE /=. rewrite /onem. field. rewrite subr_eq0; apply: contra H => /eqP rs1. 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)