no goals
α : Type u_1
β : Type u_2
γ : Type ?u.151870
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : Ring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x
rw [← add_assoc, h, h.periodic.int_mul]