English
rev commutes with succAbove: rev(succAbove p i) = succAbove(rev p)(rev i).
Русский
rev коммутирует с succAbove: rev(succAbove p i) = succAbove(rev p)(rev i).
LaTeX
$$$\forall p:\mathrm{Fin}(n+1),\forall i:\mathrm{Fin}(n),\ \mathrm{rev}(\mathrm{succAbove}\;p\;i) = \mathrm{succAbove}\; (\mathrm{rev}\;p)\; (\mathrm{rev}\;i).$$$
Lean4
/-- `rev` commutes with `succAbove`. -/
theorem rev_succAbove (p : Fin (n + 1)) (i : Fin n) : rev (succAbove p i) = succAbove (rev p) (rev i) := by
rw [succAbove_rev_left, rev_rev]