proposition: Theorem canonical_pX_ltP : forall a p, canonical (pX a p) -> ltP p (pX a pO).
proof: Proof. intros a p H'; auto. apply olist_pX_ltP; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)