proposition: Lemma q_of_r1 r : r != 1%:pr -> [q_of r, 1%:pr] = 1%:pr.
proof: Proof. move=> r1. by apply/val_inj => /=; rewrite q_of_rsE /= mulr1 p_of_r1 divff // onem_neq0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)