An exact proof term for the current goal is Sep_Subq real (λq ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, q = m :/: n).