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