no goals
α : Type u_1
β : Type ?u.5460
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f ((f^[Nat.pred n]) x) = x
rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]