English
Let i0 be a fixed element in a linearly ordered set without a minimal element. For every natural number n, the value obtained by applying the predecessor map n times and then converting to integers satisfies toZ i0 (pred^n i0) = -n.
Русский
Пусть i0 — фиксированный элемент в линейно упорядоченном множестве без минимума. Для каждого натурального числа n значение toZ i0, получаемое после применения оператора предшественника n раз к i0 и перехода к целым равно -n.
LaTeX
$$$\\forall n \\in \\mathbb{N},\\; \\operatorname{toZ}_{i_0}\\big(\\operatorname{pred}^{\\,n} i_0\\big) = -n$$$
Lean4
theorem toZ_iterate_pred [NoMinOrder ι] (n : ℕ) : toZ i0 (pred^[n] i0) = -n :=
toZ_iterate_pred_of_not_isMin n (not_isMin _)
