no goals
α : Type u_1
β : Type u_2
γ : Type ?u.215561
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - c₂)
simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg