Is there a Decision procedure for ≤ on Rationals?

[langston-barrett]

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.

[langston-barrett]

It seems like this could be implemented by assuming a Decision (x ≤ y) on the numerator/denominator type, which might be more composable of a solution. If I figure out how to do that, I'll make a pull request :)

[spitters]

Yes, that seems like the right solution.