n m : ℕ
x y : Fin (n + 1)
⊢ (∃ z, ↑(succAbove x) z = y) → y ≠ x
n m : ℕ
x y : Fin (n + 1)
⊢ (∃ z, ↑(succAbove x) z = y) ↔ y ≠ x
refine' ⟨_, exists_succAbove_eq⟩
case intro
n m : ℕ
x : Fin (n + 1)
y : Fin n
⊢ ↑(succAbove x) y ≠ x
n m : ℕ
x y : Fin (n + 1)
⊢ (∃ z, ↑(succAbove x) z = y) → y ≠ x
rintro ⟨y, rfl⟩
no goals
case intro
n m : ℕ
x : Fin (n + 1)
y : Fin n
⊢ ↑(succAbove x) y ≠ x
exact succAbove_ne _ _