no goals
α : Type u_1
β : Type u_2
γ : Type ?u.211684
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : Neg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ + c₂)
simp_all [← add_assoc]