match eq : decide (p > q) with
| true =>
  show p ≤ (if true then p else q)
  show p ≤ p
  exact le_refl
| false =>
  show p ≤ (if false then p else q)
  show p ≤ q
  have : ¬(p > q) := ofBoolUsing_eq_false eq
  have : sgn (p - q) ≄ 1 := mt gt_sgn.mpr this
  have : p ≤ q := le_sgn.mpr this
  exact this
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ if decide (p > q) = true then p else q
no goals