no goals
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Ring R
p q r : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (-p) = -eval₂ f x p
rw [eq_neg_iff_add_eq_zero, ← eval₂_add, add_left_neg, eval₂_zero]