proposition: Theorem zeroP_minusTerm : forall a : Term, zeroP (minusTerm a a).
proof: Proof. Proof using plusA multA invA divA cs A1. intros a; apply zeroP_comp_eqTerm with (a := plusTerm a (invTerm a)); auto. apply plusTerm_invTerm_zeroP; auto. apply eqTerm_sym; apply eqTerm_minusTerm_plusTerm_invTerm; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)