proposition: Theorem zerop_ddivp_ppc : forall a b : poly A0 eqA ltM, ~ zerop a -> ~ zerop b -> divp (ppcp a b) 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. intros a0 l a1 l0 H' H'0 H'1 H'2. apply divP_ppcr with (1 := cs); auto. apply canonical_nzeroP with (ltM := ltM) (p := l); auto. apply canonical_nzeroP with (ltM := ltM) (p := l0); auto. Qed.
imports: Buchberger(moreCoefStructure)