English
For p ∈ Fin(n) and i ∈ Fin(n+1) with i ≠ castSucc p, p.castSucc.succAbove (p.predAbove i) = i.
Русский
Для p ∈ Fin(n) и i ∈ Fin(n+1), если i ≠ castSucc p, то p.castSucc.succAbove(p.predAbove i) = i.
LaTeX
$$$\forall p \in \mathrm{Fin}(n),\ \forall i \in \mathrm{Fin}(n+1),\ i \neq \mathrm{castSucc}(p) \Rightarrow p.castSucc.succAbove(p.predAbove(i)) = i$$$
Lean4
/-- `succ` commutes with `predAbove`. -/
@[simp]
theorem succ_predAbove_succ (a : Fin n) (b : Fin (n + 1)) : a.succ.predAbove b.succ = (a.predAbove b).succ :=
by
obtain h | h := Fin.le_or_gt (succ a) b
· rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]
· rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]
