simp only [not_lt, nonpos_iff_eq_zero] at h
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : ¬0 < n
⊢ n = 0
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : n = 0
⊢ n = 0