proposition: Theorem minusTerm_ltT_l : forall a b c, eqT a b -> ltT a c -> ltT (minusTerm minusA a b) c.
proof: Proof. intros a b c; case a; case b; case c; unfold ltT in |- *; simpl in |- *; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)