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

State before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommMonoid R
f : R → S
c d : R
h : (PeriodEquiv f) c d
⊢ f c = f d
Tactic:
rw [← zero_add c, h, zero_add]
State after:
no goals