English
For p ∈ Fin(n+1) and i ∈ Fin(n), p.succAbove i < p iff castSucc i < p.
Русский
Для p ∈ Fin(n+1) и i ∈ Fin(n) выполняется p.succAbove i < p тогда и только если castSucc i < p.
LaTeX
$$$\forall n \in \mathbb{N}\, \forall p \in \mathrm{Fin}(n+1)\, \forall i \in \mathrm{Fin}(n),\ p.succAbove(i) < p\ \Leftrightarrow\ \mathrm{castSucc}(i) < p.$$$
Lean4
/-- Embedding `i : Fin n` into `Fin (n + 1)` using a pivot `p` that is greater
results in a value that is less than `p`. -/
theorem succAbove_lt_iff_castSucc_lt (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ castSucc i < p :=
by
rcases castSucc_lt_or_lt_succ p i with H | H
· rwa [iff_true_right H, succAbove_of_castSucc_lt _ _ H]
· rw [castSucc_lt_iff_succ_le, iff_false_right (Fin.not_le.2 H), succAbove_of_lt_succ _ _ H]
exact Fin.not_lt.2 <| Fin.le_of_lt H
