proposition: Theorem canonical_nzeroP : forall a p, canonical (pX a p) -> ~ zeroP (A:=A) A0 eqA (n:=n) a.
proof: Proof. intros a p H'; red in |- *; intros H'0; inversion H'. generalize H0; simpl in |- *; intuition; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)