proposition: Theorem eqTerm_minusTerm_plusTerm_invTerm : forall a b : Term, eqTerm (minusTerm a b) (plusTerm a (invTerm b)).
proof: Proof. Proof using multA divA cs A1 A0. intros a b; case a; case b; simpl in |- *; auto. split; auto. apply minusA_def with (1 := cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)