intro eq
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
⊢ f^[n] x = x → n = 0
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
eq : f^[n] x = x
⊢ n = 0