proposition: Theorem multTerm_assoc : forall a b c : Term, eqTerm (multTerm a (multTerm b c)) (multTerm (multTerm a b) c).
proof: Proof. Proof using plusA minusA invA divA cs A1 A0. intros a b c; case a; case b; case c; simpl in |- *; auto. intros a0 m a1 m0 a2 m1; split; auto. apply multA_assoc with (1 := cs); auto. apply mult_mon_assoc. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)