Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq2 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x y : R
⊢ g (x * y + 1) - g (x * y - 1) = g (x + y) - g (x - y)
Tactic:
rw [hg.is_good, hg.alt_good, add_sub_add_left_eq_sub]
State after:
no goals