proposition: Lemma ltT_not_ltT : forall x y : Term A n, ltT x y -> ~ ltT y x.
proof: Proof. Proof using os. intros x y H'; red in |- *; intros H'0; absurd (ltT x x); auto. apply ltT_trans with (y := 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)