proposition: Lemma poly_eq_ind (P: poly → poly → Prop) (case_0: ∀ p p', poly_eq_zero p → poly_eq_zero p' → P p p') (case_cons: ∀ x x' p p', x = x' → p = p' → P p p' → P (x::p) (x'::p')) p: ∀ p', p = p' → P p p'.
proof: Proof. induction p as [|x p IH]; intros [|x' p'] eqxy. 1,2,3: now apply case_0. destruct eqxy. apply case_cons; auto. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring