English
The natural numbers are equipped with a PredOrder structure whose pred operation agrees with the usual predecessor.
Русский
Натуральные числа оснащены структурой PredOrder, у которой операция predecessor совпадает с обычным предшественником.
LaTeX
$$$\\\\operatorname{PredOrder}(\\\\mathbb N) \\\\text{ with } \\\\operatorname{pred} = \\operatorname{pred}_{\\\\mathbb N}.$$$
Lean4
@[instance]
abbrev instPredOrder : PredOrder ℕ where
pred := pred
pred_le := pred_le
min_of_le_pred {a}
ha := by
cases a
· exact isMin_bot
· exact (not_succ_le_self _ ha).elim
le_pred_of_lt {a} {b}
h := by
cases b
· exact (a.not_lt_zero h).elim
· exact le_of_succ_le_succ h
