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