match eq : decide (p < q) with
| true =>
  show (if true then p else q) ≤ q
  show p ≤ q
  have : p < q := ofBoolUsing_eq_true eq
  have : p ≤ q := le_cases.mpr (Or.inl this)
  exact this
| false =>
  show (if false then p else q) ≤ q
  show q ≤ q
  exact le_refl
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≤ q
no goals