proposition: Lemma eqT_not_ltT : forall x y : Term A n, ltT x y -> ~ eqT x y.
proof: Proof. Proof using os. unfold eqT, ltT, not in |- *; simpl in |- *; intros x y H Q; absurd (ltM (T2M x) (T2M y)); auto; rewrite Q; 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)