no goals
α : Type u_1
β : Type ?u.3547
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
⊢ (f^[m % n]) x = (f^[m]) x
conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]