proposition: Theorem divp_trans : transitive (poly A0 eqA ltM) divp.
proof: Proof. Proof using plusA minusA invA cs A1. red in |- *. intros x y z; case x; case y; case z. intros x0 c x1 c0 x2 c1; generalize c c0 c1; case x0; case x1; case x2; simpl in |- *; auto. intros a l a0 l0 H' H'0 H'1 H'2; elim H'2. intros a l a0 l0 a1 l1 H' H'0 H'1 H'2 H'3. apply (divP_trans _ _ _ _ _ _ _ _ _ cs n) with (y := a0); auto. Qed.
imports: Buchberger(moreCoefStructure)