proposition: Theorem eqTerm_trans : transitive Term eqTerm.
proof: Proof. Proof using plusA multA minusA invA divA cs A1 A0. red in |- *. intros x y z; case x; case y; case z; simpl in |- *; intuition. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := a0); auto. rewrite H2; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)