proposition: Theorem multTerm_com : forall a b : Term, eqTerm (multTerm a b) (multTerm b a).
proof: Proof. Proof using plusA minusA invA divA cs A1 A0. intros a b; case a; case b; simpl in |- *; auto. intros a0 m a1 m0; split; auto. apply mult_mon_com. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)