repeat rw [Pi.neg_apply]
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ (-f) ((-f) x * (-f) y) + (-f) (x + y) = (-f) (x * y)
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)