English
Let p ∈ Fin n, i ∈ Fin(n+1) and h be succ p ≤ i. Then p.predAbove i = i.pred (Fin.ne_of_gt (Fin.lt_of_lt_of_le (succ p) h)).
Русский
Пусть p ∈ Fin(n), i ∈ Fin(n+1) и h: succ p ≤ i. Тогда p.predAbove i = i.pred (Fin.ne_of_gt (Fin.lt_of_lt_of_le (succ p) h)).
LaTeX
$$$ \\forall p \\in \\mathrm{Fin}(n), \\forall i \\in \\mathrm{Fin}(n+1),\\ h:\\ \\operatorname{succ}(p) \\le i \\\\ :\\ p.predAbove i = i.pred \\bigl( \\operatorname{Fin.ne\\_of\\_gt} \\bigl( \\operatorname{Fin.lt\\_of\\_lt\\_of\\_le} (\\operatorname{succ\\_pos} (), h) \\bigr) \\bigr) $$$
Lean4
theorem predAbove_of_succ_le (p : Fin n) (i : Fin (n + 1)) (h : succ p ≤ i) :
p.predAbove i = i.pred (Fin.ne_of_gt <| Fin.lt_of_lt_of_le (succ_pos _) h) :=
predAbove_of_castSucc_lt _ _ (castSucc_lt_iff_succ_le.mpr h)
