English
If toZ i0 i ≤ toZ i0 j, then i ≤ j.
Русский
Если toZ i0 i ≤ toZ i0 j, то i ≤ j.
LaTeX
$$toZ(i_0,i) \le toZ(i_0,j) \implies i \le j$$
Lean4
theorem le_of_toZ_le {j : ι} (h_le : toZ i0 i ≤ toZ i0 j) : i ≤ j :=
by
rcases le_or_gt i0 i with hi | hi <;> rcases le_or_gt i0 j with hj | hj
· rw [← iterate_succ_toZ i hi, ← iterate_succ_toZ j hj]
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ _) (Int.toNat_le_toNat h_le)
· exact absurd ((toZ_neg hj).trans_le (toZ_nonneg hi)) (not_lt.mpr h_le)
· exact hi.le.trans hj
· rw [← iterate_pred_toZ i hi, ← iterate_pred_toZ j hj]
refine Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat ?_)
exact Int.neg_le_neg h_le
