English
Let p,i ∈ Fin(n+1) with p ≤ i and hp ≠ 0. Then (pred p hp).predAbove i = pred i (Fin.ne_of_gt (Fin.lt_of_lt_of_le (Fin.pos_iff_ne_zero.2 hp) h)).
Русский
Пусть p,i ∈ Fin(n+1) и p ≤ i, hp ≠ 0. Тогда (pred p hp).predAbove i = pred i (Fin.ne_of_gt (Fin.lt_of_lt_of_le (Fin.pos_iff_ne_zero.2 hp) h)).
LaTeX
$$$ \\forall p,i \\in \\mathrm{Fin}(n+1),\\ h:\\ p \\le i,\\ hp:\\ hp \\neq 0 \\\\ :\\ (\\operatorname{pred}~p~hp).predAbove(i) = \\operatorname{pred} i \\bigl( \\operatorname{Fin.ne\\_of\\_gt} ( \\operatorname{Fin.lt\\_of\\_lt\\_of\\_le} (\\operatorname{Fin.pos\\_iff\\_ne\\_zero}.2 hp) h)\\bigr) $$$
Lean4
theorem predAbove_pred_of_le (p i : Fin (n + 1)) (h : p ≤ i) (hp : p ≠ 0) :
(pred p hp).predAbove i = pred i (Fin.ne_of_gt <| Fin.lt_of_lt_of_le (Fin.pos_iff_ne_zero.2 hp) h) := by
rw [predAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)]
