proposition: Theorem ltT_trans : transitive (Term A n) ltT.
proof: Proof. Proof using os. unfold transitive, ltT in |- *; auto. intros x y z H' H'0; apply (ltM_trans _ _ _ _ os) with (y := T2M y); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)