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 + 0) ↔ f (x + c) = f x
Tactic:
rw [add_zero]
State after:
no goals