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