proposition: Theorem divP_ppc : forall a b c : poly A0 eqA ltM, divp a b -> divp a c -> divp a (ppcp b c).
proof: Proof. intros a b c; (case a; case b; case c). intros x c0 x0 c1 x1 c2; generalize c0 c1 c2; case x; case x0; case x1; simpl in |- *; auto. intros a0 l a1 l0 a2 l1 H' H'0 H'1 H'2 H'3. elim ppc_is_ppcm with (1 := cs) (a := a1) (b := a2); auto. apply canonical_nzeroP with (ltM := ltM) (p := l0); auto. apply canonical_nzeroP with (ltM := ltM) (p := l1); auto. Qed.
imports: Buchberger(moreCoefStructure)