proposition: Lemma RratE (x : rat) (a : Qint) : refines Rrat x a -> x = a.1%:~R / (val a.2)%:~R.
proof: Proof. by move=> rxa; rewrite -[x]/(spec_id _) [spec_id _]refines_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop order) mathcomp(ssralg ssrint ssrnum rat) CoqEAL(hrel param refinements pos)