proposition: Theorem eqTerm_sym : symmetric Term eqTerm.
proof: Proof. Proof using plusA multA minusA invA divA cs A1 A0. red in |- *. intros x y; case x; case y; simpl in |- *; intuition. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)