proposition: Theorem multTerm_zeroP_div : forall a b : Term, zeroP (multTerm a b) -> zeroP a \/ zeroP b.
proof: Proof. Proof using plusA minusA invA eqA_dec divA cs A1. intros a b; case a; case b; simpl in |- *; auto. intros a0 m a1 m0 H. apply A_sep with (2 := eqA_dec) (1 := cs); auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)