Theorem: Imo2017P2.good_special_equality (Compfiles/Imo2017P2.lean)

State before:
R : Type u_1
inst✝ : Ring 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