English
predAbove also commutes with reverse on Fin: p.rev.predAbove i = (p.predAbove i.rev).rev.
Русский
predAbove взаимно согласовано с разворотом: p.rev.predAbove i = (p.predAbove i.rev).rev.
LaTeX
$$$\forall p:\mathrm{Fin}(n),\forall i:\mathrm{Fin}(n+1),\ p.rev.predAbove\;i = (p.predAbove\; i.rev).rev.$$$
Lean4
theorem predAbove_rev_left (p : Fin n) (i : Fin (n + 1)) : p.rev.predAbove i = (p.predAbove i.rev).rev :=
by
obtain h | h := (rev i).succ_le_or_le_castSucc p
·
rw [predAbove_of_succ_le _ _ h, rev_pred, predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)),
castPred_inj, rev_rev]
·
rw [predAbove_of_le_castSucc _ _ h, rev_castPred, predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)),
pred_inj, rev_rev]
