proposition: Corollary poly_eq_zero_cons x p: poly_eq_zero (x::p) ↔ x = 0 ∧ poly_eq_zero p.
proof: Proof. unfold poly_eq_zero, compose; cbn; rewrite all_cons. intuition now symmetry. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring