proposition: Theorem divp_nzeropr : forall a b : poly A0 eqA ltM, divp a b -> ~ zerop b.
proof: Proof. intros a b; (case a; case b). intros x c0 x0 c1; generalize c0 c1; case x; case x0; simpl in |- *; auto. Qed.
imports: Buchberger(moreCoefStructure)