proposition: Theorem divp_ppc : forall a b c : poly A0 eqA ltM, divp (ppcp a b) c -> divp (ppcp b a) 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. apply divP_eqTerm_comp with (1 := cs) (a := ppc (A:=A) A1 (n:=n) a0 a1); auto. Qed.
imports: Buchberger(moreCoefStructure)