proposition: Lemma ltT_not_eqT : forall x y : Term A n, eqT x y -> ~ ltT x y.
proof: Proof. Proof using os. unfold eqT, ltT in |- *; simpl in |- *; intros x y H; rewrite H; auto. apply ltM_nonrefl with (1 := os). Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)