English
Every Fin n carries a natural SuccOrder structure extending the usual order on indices; the order is defined by the last element and the successor relation.
Русский
Каждый Fin n наделён естественной структурой SuccOrder, расширяющей обычный порядок по индексам; порядок задаётся последним элементом и отношением successor.
LaTeX
$$$\mathrm{SuccOrder}(\mathrm{Fin}(n))$$$
Lean4
instance : ∀ {n : ℕ}, SuccOrder (Fin n)
| 0 => by constructor <;> intro a <;> exact elim0 a
| n + 1 =>
SuccOrder.ofCore (Fin.lastCases (Fin.last n) Fin.succ)
(fun {i} hi j ↦ by
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (by simpa using hi)
simp [castSucc_lt_iff_succ_le])
(fun i hi ↦ by
obtain rfl : i = Fin.last n := by simpa using hi
simp)
