proposition: Theorem eqTerm_multTerm_comp : forall a b c d : Term, eqTerm a b -> eqTerm c d -> eqTerm (multTerm a c) (multTerm b d).
proof: Proof. Proof using plusA minusA invA divA cs A1 A0. intros a b c d; case a; case b; case c; case d; simpl in |- *; auto. intros a1 m1 a2 m2 a3 m3 a4 m4; intros H1; case H1; intros H2 H3 H4; case H4; intros H5 H6; split; auto. rewrite H3; rewrite H6; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)