English
The reverse operation commutes with predAbove: (predAbove p i).rev = predAbove p.rev i.rev.
Русский
Обратное отображение коммутирует с predAbove: (predAbove p i).rev = predAbove p.rev i.rev.
LaTeX
$$$\\forall n,\\; p \\in \\mathrm{Fin}(n),\\; i \\in \\mathrm{Fin}(n+1):\\; (predAbove\\ p\\ i).rev = predAbove\\ (p.rev)\\ (i.rev).$$$
Lean4
/-- `rev` commutes with `predAbove`. -/
theorem rev_predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : (predAbove p i).rev = predAbove p.rev i.rev := by
rw [predAbove_rev_left, rev_rev]