proposition: Lemma poly_eq_zero_plus_l p q: poly_eq_zero p → p + q = q.
proof: Proof. intro eqp; revert q. induction eqp as [|x p eqx eqp IH] using poly_eq_zero_ind. { easy. } intros [|y q]. { cbn -[poly_eq_zero]. rewrite poly_eq_zero_cons; auto. } cbn; split; auto. ring [eqx]. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring