English
Applying predAbove after casting p to Fin(n) and then applying succAbove to i recovers i: p.predAbove((castSucc p).succAbove i) = i for i in Fin n.
Русский
Применение predAbove после castSucc и затем succAbove восстанавливает i: p.predAbove((castSucc p).succAbove i) = i для i ∈ Fin(n).
LaTeX
$$$\forall p \in \mathrm{Fin}(n),\ \forall i \in \mathrm{Fin}(n),\ p.predAbove((\mathrm{castSucc}\,p).succAbove(i)) = i$$$
Lean4
/-- Sending `Fin n` into `Fin (n + 1)` with a gap at `p`
then back to `Fin n` by subtracting one from anything above `p` is the identity. -/
@[simp]
theorem predAbove_succAbove (p : Fin n) (i : Fin n) : p.predAbove ((castSucc p).succAbove i) = i :=
by
obtain h | h := p.le_or_gt i
· rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]
· rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]
