proposition: Corollary poly_eq_zero_plus p q: poly_eq_zero p → poly_eq_zero q → poly_eq_zero (p+q).
proof: Proof. intro. rewrite <- !poly_eq_p_zero; intro. now rewrite poly_eq_zero_plus_l. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring