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

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x y : R
⊢ f (x * y - 1) = f x * f y + f (x - y)
Tactic:
rw [← h y, sub_eq_add_neg x, ← hf.is_good, mul_neg, neg_add_eq_sub, ← neg_sub, h]
State after:
no goals