proposition: Theorem T1_eqT : forall a b : Term, eqTerm a T1 -> eqT b (multTerm a b).
proof: Proof. intros a b; case a; case b; simpl in |- *; auto. intros a1 m1 a2 m2 H1; case H1; intros H2 H3; auto. rewrite H3; auto. unfold eqT in |- *; simpl in |- *; apply sym_eq; unfold M1 in |- *; apply mult_mon_zero_l. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)