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

State before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommGroup R
f : R → S
c d : R
h : (PeriodEquiv f) c d
x : R
⊢ f (x + (c - d)) = f (x + 0)
Tactic:
rw [← add_comm_sub, h, sub_add_cancel, add_zero]
State after:
no goals

State before:
R : Type u_1
S : Sort u_2
inst✝ : AddCommGroup R
f : R → S
c d : R
h : (PeriodEquiv f) (c - d) 0
x : R
⊢ f (x + c) = f (x + d)
Tactic:
rw [← add_add_sub_cancel x c d, h, add_zero]
State after:
no goals