English
Finite index sets Fin(n) inherit a PredOrder structure with pred defined by Pred = Fin.cases(0, Fin.castSucc); namely, pred(0)=0 and pred(i+1)=castSucc(i).
Русский
Множества Fin(n) наследуют предикаторную структуру PredOrder, pred задан как Pred = Fin.cases(0, Fin.castSucc); pred(0)=0, pred(i+1)=castSucc(i).
LaTeX
$$$\mathrm{PredOrder}(\mathrm{Fin}(n))\,\text{with }\ pred(i) = \mathrm{Fin.cases}(0,\mathrm{Fin.castSucc})(i)$$$
Lean4
instance : ∀ {n : ℕ}, PredOrder (Fin n)
| 0 => by
constructor <;>
first
| intro a; exact elim0 a
| n + 1 =>
PredOrder.ofCore (Fin.cases 0 Fin.castSucc)
(fun {i} hi j ↦ by
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (by simpa using hi)
simp [le_castSucc_iff])
(fun i hi ↦ by
obtain rfl : i = 0 := by simpa using hi
rfl)
