no goals
R : Type u_1
inst✝ : Semiring R
p q : R[X]
h : mirror p = 0
⊢ p = 0
rw [← p.mirror_mirror, h, mirror_zero]
no goals
R : Type u_1
inst✝ : Semiring R
p q : R[X]
h : p = 0
⊢ mirror p = 0
rw [h, mirror_zero]