English
The value p.succAbove(i) is never equal to p for any p ∈ Fin(n+1) and i ∈ Fin(n).
Русский
Можно показать, что p.succAbove(i) никогда не равно p для любых p ∈ Fin(n+1) и i ∈ Fin(n).
LaTeX
$$$\forall p \in \mathrm{Fin}(n+1),\ \forall i \in \mathrm{Fin}(n),\ p.succAbove(i) \neq p.$$$
Lean4
/-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)`
never results in `p` itself -/
@[simp]
theorem succAbove_ne (p : Fin (n + 1)) (i : Fin n) : p.succAbove i ≠ p :=
by
rcases p.castSucc_lt_or_lt_succ i with (h | h)
· rw [succAbove_of_castSucc_lt _ _ h]
exact Fin.ne_of_lt h
· rw [succAbove_of_lt_succ _ _ h]
exact Fin.ne_of_gt h
