proposition: Theorem plusTerm_invTerm_zeroP : forall a : Term, zeroP (plusTerm a (invTerm a)).
proof: Proof. Proof using multA minusA divA cs A1. intros a; case a; simpl in |- *; auto. intros; apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); apply invA_plusA with (1 := cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)