proposition: Theorem ltP_pX_canonical : forall a p, canonical p -> ~ zeroP (A:=A) A0 eqA (n:=n) a -> ltP p (pX a pO) -> canonical (pX a p).
proof: Proof. Proof using eqA_dec. intros a p H' H'0 H'1; split; auto. apply ltP_pX_olist; auto. inversion H'. generalize H0 H'0; simpl in |- *; case (zeroP_dec A A0 eqA eqA_dec n 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)