have : a < b ∨ a ≃ b := match this with
| isTrue (_ : a ≃ b) =>
  Or.inr ‹a ≃ b›
| isFalse (_ : a ≄ b) =>
  have : a < b := lt_iff_le_neqv.mpr (And.intro ‹a ≤ b› ‹a ≄ b›)
  Or.inl ‹a < b›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a ≤ b
this : Decidable (a ≃ b)
⊢ a < b ∨ a ≃ b
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a ≤ b
this✝ : Decidable (a ≃ b)
this : a < b ∨ a ≃ b
⊢ a < b ∨ a ≃ b