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