proposition: Theorem canonical_ltT : forall l a b, canonical (l ++ pX a (pX b pO)) -> ltT b a.
proof: Proof. intros l a b H'; auto. apply olist_ltT with (l := l); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)