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