English
Let p be an element of Fin n and i an element of Fin(n+1). If i is at most castSucc p, then p.predAbove i equals i.castPred applied to a witness that i is not less than the last element, i.e. p.predAbove i = i.castPred (Fin.ne_of_lt (Fin.lt_of_le_of_lt h (castSucc_lt_last _))).
Русский
Пусть p ∈ Fin(n) и i ∈ Fin(n+1). Если i не больше castSucc p, тогда p.predAbove i равно i.castPred применительно к доказательству того, что i не меньше последнего элемента: p.predAbove i = i.castPred (Fin.ne_of_lt (Fin.lt_of_le_of_lt h (castSucc_lt_last _))).
LaTeX
$$$ \\forall p \\in \\mathrm{Fin}(n), \\forall i \\in \\mathrm{Fin}(n+1),\\ h:\\ i \\le \\operatorname{castSucc}(p) \\\\ :\\ p.predAbove i = i.castPred \\bigl( \\operatorname{Fin.ne\_of\_lt} \\bigl( \\operatorname{Fin.lt\_of\_le\_of\_lt} (h, \\operatorname{castSucc\_lt\_last}) \\bigr) \\bigr) $$$
Lean4
theorem predAbove_of_le_castSucc (p : Fin n) (i : Fin (n + 1)) (h : i ≤ castSucc p) :
p.predAbove i = i.castPred (Fin.ne_of_lt <| Fin.lt_of_le_of_lt h <| castSucc_lt_last _) :=
dif_neg <| Fin.not_lt.2 h
