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