Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.period_imp_zero₀ (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : RShiftGood23 g
c : R
h : ∀ (x : R), g (x + c) = g x
x : R
⊢ g (x + c) = g (x + 0)
Tactic:
rw [h, add_zero]
State after:
no goals