English
If none of the iterations pred^[n] i0 are minimal, then toZ i0 (pred^[n] i0) = -n.
Русский
Если ни одна из итераций pred^[n] i0 не минимальна, то toZ i0 (pred^[n] i0) = -n.
LaTeX
$$toZ(i_0, pred^{[n]}(i_0)) = -n$$
Lean4
theorem toZ_iterate_pred_of_not_isMin (n : ℕ) (hn : ¬IsMin (pred^[n] i0)) : toZ i0 (pred^[n] i0) = -n :=
by
rcases n with - | n
· simp
have : pred^[n.succ] i0 < i0 :=
by
refine lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn ?_
have h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0 := by rwa [Function.iterate_zero, id]
exact isMin_iterate_pred_of_eq_of_ne h_pred_eq_pred (Nat.succ_ne_zero n)
let m := (-toZ i0 (pred^[n.succ] i0)).toNat
have h_eq : pred^[m] i0 = pred^[n.succ] i0 := iterate_pred_toZ _ this
by_cases hmn : m = n + 1
· nth_rw 2 [← hmn]
rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]
rw [neg_neg]
exact Int.natCast_nonneg _
· suffices IsMin (pred^[n.succ] i0) from absurd this hn
exact isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)
