Is there a Decision procedure for ≤ on Rationals?

I'm trying to write a proof involving an inequality between rational numbers, and I'd love to be able to destruct (decide (x ≤ 0)). However, when I attempt that, I get the following error:

Unable to satisfy the following constraints:
In environment:
R : Type
e : Equiv R
plus0 : Plus R
mult0 : Mult R
zero0 : Zero R
one0 : One R
neg : Negate R
recip0 : DecRecip R
U : RationalsToFrac R
H : Rationals R
x, y : R → R
k_Ω : R
k_Ω_neq_0 : k_Ω ≠ 0
n0_Ω : R
HΩ : ∀ n : R, n0_Ω ≤ n → k_Ω * y n ≤ x n
n : R
n_geq_n0_Ω : n0_Ω ≤ n

?Le : "Le R"
?Zero : "Zero R"
?Decision : "Decision (k_Ω ≤ 0)"

Obviously, the Le and Zero errors are red herrings, but I can't actually seem to find a decision procedure for Rationals, other than on actual instances.

Start by inspecting the abstract Rationals, Le, Zero, and Decision interfaces, then compare them with any decision procedures available for concrete rational instances. Verify whether the reported destruct (decide (x ≤ 0)) can be supported for the abstract setting; done means the missing procedure is exposed or the limitation is documented.