proposition: Lemma poly_eq_zero_ind (P: poly → Prop) (case_nil: P []) (casecons: ∀ x p, x = 0 → poly_eq_zero p → P p → P (x::p)) p: poly_eq_zero p → P p.
proof: Proof. induction p as [|x p IH]; auto. intros [??]%poly_eq_zero_cons. eauto. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring