have : a < b + 1 := match ‹a < b ∨ a ≃ b› with
| Or.inl (_ : a < b) => Rel.trans ‹a < b› ‹b < b + 1›
| Or.inr (_ : a ≃ b) => AA.substLFn (Rel.symm ‹a ≃ b›) ‹b < b + 1›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a ≤ b
this✝ : b < b + 1
this : a < b ∨ a ≃ b
⊢ a < b + 1
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a ≤ b
this✝¹ : b < b + 1
this✝ : a < b ∨ a ≃ b
this : a < b + 1
⊢ a < b + 1