Lean4
/-- If the order has neither bot nor top, `toZ` defines an `OrderIso` between `ι` and `ℤ`. -/
noncomputable def orderIsoIntOfLinearSuccPredArch [NoMaxOrder ι] [NoMinOrder ι] [hι : Nonempty ι] : ι ≃o ℤ
where
toFun := toZ hι.some
invFun n := if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some
left_inv
i := by
rcases le_or_gt hι.some i with hi | hi
· have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi
simp_rw [if_pos h_nonneg]
exact iterate_succ_toZ i hi
· have h_neg : toZ hι.some i < 0 := toZ_neg hi
simp_rw [if_neg (not_le.mpr h_neg)]
exact iterate_pred_toZ i hi
right_inv
n := by
rcases le_or_gt 0 n with hn | hn
· simp_rw [if_pos hn]
rw [toZ_iterate_succ]
exact Int.toNat_of_nonneg hn
· simp_rw [if_neg (not_le.mpr hn)]
rw [toZ_iterate_pred]
simp only [hn.le, Int.toNat_of_nonneg, Int.neg_nonneg_of_nonpos, Int.neg_neg]
map_rel_iff' := by intro i j; exact toZ_le_iff i j
