ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i0 ≤ i
⊢ (succ^[Nat.find (_ : ∃ n, (succ^[n]) i0 = i)]) i0 = i
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i0 ≤ i
⊢ (succ^[Int.toNat (toZ i0 i)]) i0 = i
rw [toZ_of_ge hi, Int.toNat_coe_nat]
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i0 ≤ i
⊢ (succ^[Nat.find (_ : ∃ n, (succ^[n]) i0 = i)]) i0 = i
exact Nat.find_spec (exists_succ_iterate_of_le hi)