simp at hper
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : ∀ (x : α), x ∈ {x | ∃ n > 0, f^[n] x = x} ↔ x ∈ ∅
eq : f^[n] x = x
⊢ n = 0
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x : α) (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0