English
For p ∈ Fin(n+1) and i ∈ Fin n, (rev p).succAbove i equals (rev p).succAbove i rev, i.e., p.rev.succAbove i = (p.succAbove i.rev).rev.
Русский
Для p ∈ Fin(n+1) и i ∈ Fin n выполняется (rev p).succAbove i = (p.succAbove i.rev).rev.
LaTeX
$$$\forall p:\mathrm{Fin}(n+1),\forall i:\mathrm{Fin}(n),\ (\mathrm{rev} \; p) \,\mathrm{succAbove}\, i = (\mathrm{rev}\, p)^{\mathrm{succAbove}}(i) =$$$
Lean4
theorem succAbove_rev_left (p : Fin (n + 1)) (i : Fin n) : p.rev.succAbove i = (p.succAbove i.rev).rev :=
by
obtain h | h := (rev p).succ_le_or_le_castSucc i
· rw [succAbove_of_succ_le _ _ h, succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]
·
rw [succAbove_of_le_castSucc _ _ h, succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc,
rev_rev]
