ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i < i0
⊢ (pred^[Nat.find (_ : ∃ n, (pred^[n]) i0 = i)]) i0 = i
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i < i0
⊢ (pred^[Int.toNat (-toZ i0 i)]) i0 = i
rw [toZ_of_lt hi, neg_neg, Int.toNat_coe_nat]
no goals
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i✝ i : ι
hi : i < i0
⊢ (pred^[Nat.find (_ : ∃ n, (pred^[n]) i0 = i)]) i0 = i
exact Nat.find_spec (exists_pred_iterate_of_le hi.le)