have : sgn (p - q) ≄ -1 := mt lt_sgn.mpr this
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this : ¬p < q
⊢ q ≤ p
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this✝ : ¬p < q
this : sgn (p - q) ≄ -1
⊢ q ≤ p