proposition: Theorem plusTerm_com : forall x y : Term, eqT x y -> eqTerm (plusTerm x y) (plusTerm y x).
proof: Proof. Proof using multA minusA invA divA cs A1 A0. intros a b; case a; case b; simpl in |- *; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)