proposition: Theorem T1_nz : ~ zeroP T1.
proof: Proof. Proof using plusA multA minusA invA divA cs. simpl in |- *; auto. apply A1_diff_A0 with (1 := cs). Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)