proposition: Theorem multTerm_ltT_l : forall m1 m2 m3, ltT m1 m2 -> ltT (multTerm multA m3 m1) (multTerm multA m3 m2).
proof: Proof. Proof using os. intros a b c; case a; case b; case c; unfold ltT in |- *; simpl in |- *; auto. intros a0 m a1 m0 a2 m1 H. apply ltM_plusl with (1 := os); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)