succ_ne_last_of_lt — Mathlib

English

If p and i are in Fin(n) and i < p, then the successor of i is not the last element of Fin(n).

Русский

Если p и i принадлежат Fin(n) и i < p, то succ(i) ≠ last(n).

LaTeX

$$$$ \\forall n \\in \\mathbb{N}, \\forall p,i \\in \\mathrm{Fin}(n): i < p \\implies \\operatorname{succ}(i) \\neq \\operatorname{last}(n). $$$$

Lean4

theorem succ_ne_last_of_lt {p i : Fin n} (h : i < p) : succ i ≠ last n :=
  by
  cases n
  · exact i.elim0
  · rw [succ_ne_last_iff, Ne, Fin.ext_iff]
    exact ((le_last _).trans_lt' h).ne

Похожие утверждения