match decide (p > q) with
| true =>
  apply Or.inl
  show (if true then p else q) ≃ p
  show p ≃ p
  exact eqv_refl
| false =>
  apply Or.inr
  show (if false then p else q) ≃ q
  show q ≃ q
  exact eqv_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) ≃ p ∨ (if decide (p > q) = true then p else q) ≃ q
no goals