proposition: Lemma ratR_eq a : {r | a = (r.1%:Q / r.2.+1%:Q)%R & a * r.2.+1 == r.1}.
proof: Proof. have [d Dd] := denqP a; exists (numq a, d); rewrite -Dd ?divq_num_den //=. by rewrite ratRE mulRAC mulRC (mulRC (numq a)) pmulKR ?Dd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)