case inl
n m : ℕ
x y : Fin (n + 1)
h : x ≠ y
hlt : x < y
⊢ ∃ z, ↑(succAbove y) z = x

case inr
n m : ℕ
x y : Fin (n + 1)
h : x ≠ y
hlt : y < x
⊢ ∃ z, ↑(succAbove y) z = x
n m : ℕ
x y : Fin (n + 1)
h : x ≠ y
⊢ ∃ z, ↑(succAbove y) z = x
cases' h.lt_or_lt with hlt hlt
no goals
case inl
n m : ℕ
x y : Fin (n + 1)
h : x ≠ y
hlt : x < y
⊢ ∃ z, ↑(succAbove y) z = x

case inr
n m : ℕ
x y : Fin (n + 1)
h : x ≠ y
hlt : y < x
⊢ ∃ z, ↑(succAbove y) z = x
exacts [⟨_, succAbove_castLT hlt⟩, ⟨_, succAbove_pred hlt⟩]