proposition: Lemma poly_eq_zero_trans p q: poly_eq_zero p → poly_eq_zero q → p = q.
proof: Proof. revert q. induction p as [|x p IH]; intros ? eqp eqq; auto. destruct q as [|y q]; auto. rewrite poly_eq_zero_cons in *. rewrite <- poly_eq_cons. destruct eqp as [-> ?], eqq as [-> ?]; split; eauto. now apply IH. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring