proposition: Theorem nZero_invTerm_nZero : forall a : Term, ~ zeroP a -> ~ zeroP (invTerm a).
proof: Proof. Proof using plusA multA minusA divA cs A1. intros a H'; red in |- *; intros H'0; absurd (zeroP a); auto. apply zeroP_comp_eqTerm with (a := invTerm (invTerm a)); auto. apply zeroP_invTerm_zeroP; auto. apply eqTerm_sym; apply invTerm_invol; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)