Theorem: IMOSL.IMO2012A5.PeriodEquiv.zero_right' (IMOSLLean4/IMO2012/A5/A5General/A5Periodic.lean)

State before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommMonoid R
f : R → S
c x : R
⊢ f (x + c) = f x ↔ f (c + x) = f x
Tactic:
rw [add_comm]
State after:
no goals