proposition: Theorem nZero_invTerm_T1 : ~ zeroP (invTerm T1).
proof: Proof. Proof using plusA multA minusA divA cs. apply nZero_invTerm_nZero; auto. exact T1_nz. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)