proposition: Corollary poly_eq_zero_plus_r p q: poly_eq_zero q → p + q = p.
proof: Proof. rewrite commutativity. apply poly_eq_zero_plus_l. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring