Theorem: IMOSL.IMO2017A6.good_special_equality (IMOSLLean4/IMO2017/A6/A6.lean)

State before:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
h0 : x * y = 1
⊢ f (f (x + 1) * f (y + 1)) = 0
Tactic:
rw [← add_left_eq_self, h, add_one_mul x, mul_add_one x, h0, add_comm 1 x]
State after:
no goals