have h2 := good_special_equality h h1
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
⊢ f (f 0 ^ 2) = 0
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
h2 : f (f (-1 + 1) * f (-1 + 1)) = 0
⊢ f (f 0 ^ 2) = 0