proposition: Theorem canonical_imp_canonical : forall l a, canonical (pX a l) -> canonical l.
proof: Proof. intros l a H'. split; auto. apply olist_X with (a := a); auto. elim H'; simpl in |- *; intuition. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)