proposition: Theorem canonical_imp_in_nzero : forall p : list (Term A n), canonical p -> forall a : Term A n, In a p -> ~ zeroP (A:=A) A0 eqA (n:=n) a.
proof: Proof. intros p; elim p; auto. intros a l H' H'0 a0 H'1; elim H'1; auto. intros H'2; rewrite <- H'2. apply canonical_nzeroP with (p := l); auto. intros H'2; auto. apply H'; auto. apply canonical_imp_canonical with (a := a); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)