toZ_iterate_succ_of_not_isMax — Mathlib

English

If none of the iterates succ^[n] i0 are maximal, then toZ i0 (succ^[n] i0) = n.

Русский

Если ни одна из итераций succ^[n] i0 не является максимальной, то toZ i0 (succ^[n] i0) = n.

LaTeX

$$toZ(i_0, succ^{[n]}(i_0)) = n \text{, assuming } \lnot IsMax(succ^{[n]}(i_0))$$

Lean4

theorem toZ_iterate_succ_of_not_isMax (n : ℕ) (hn : ¬IsMax (succ^[n] i0)) : toZ i0 (succ^[n] i0) = n :=
  by
  let m := (toZ i0 (succ^[n] i0)).toNat
  have h_eq : succ^[m] i0 = succ^[n] i0 := iterate_succ_toZ _ (le_succ_iterate _ _)
  by_cases hmn : m = n
  · nth_rw 2 [← hmn]
    rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]
    exact Int.natCast_nonneg _
  suffices IsMax (succ^[n] i0) from absurd this hn
  exact isMax_iterate_succ_of_eq_of_ne h_eq.symm (Ne.symm hmn)

Похожие утверждения