toZ_iterate_pred_ge — Mathlib

English

For every n, -(n) ≤ toZ i0 (pred^[n] i0).

Русский

-n ≤ toZ i0 (pred^[n] i0) для всех n.

LaTeX

$$-(n) \le toZ(i_0, pred^{[n]}(i_0))$$

Lean4

theorem toZ_iterate_pred_ge (n : ℕ) : -(n : ℤ) ≤ toZ i0 (pred^[n] i0) :=
  by
  rcases le_or_gt i0 (pred^[n] i0) with h | h
  · have h_eq : pred^[n] i0 = i0 := le_antisymm (pred_iterate_le _ _) h
    rw [h_eq, toZ_of_eq]
    cutsat
  · rw [toZ_of_lt h]
    refine Int.neg_le_neg ?_
    norm_cast
    exact Nat.find_min' _ rfl

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