no goals
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ support (update p n a) = insert n (support p)
classical rw [support_update, if_neg ha]
no goals
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ support (update p n a) = insert n (support p)
rw [support_update, if_neg ha]