no goals
α : Type u_1
β : Type u_2
γ : Type ?u.90191
f g : α → β
c c₁ c₂ x : α
inst✝ : AddMonoid α
h : Periodic f c
n : ℕ
⊢ Periodic f (n • c)
induction n <;> simp_all [Nat.succ_eq_add_one, add_nsmul, ← add_assoc, zero_nsmul]