proposition: Lemma eqT_compat_ltTr : forall a b c : Term A n, eqT b c -> ltT a b -> ltT a c.
proof: Proof. unfold eqT in |- *; unfold ltT in |- *; intros a b c H; rewrite H; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)