proposition: Theorem Red_divp : forall (L : list (poly A0 eqA ltM)) (p : poly A0 eqA ltM), In p L -> ~ zerop A A0 eqA n ltM p -> exists q : poly A0 eqA ltM, In q (Red L) /\ divp A A0 eqA multA divA n ltM p q /\ ~ zerop A A0 eqA n ltM q.
proof: Proof. intros L p H' H'0. lapply (redacc_divp L nil p); auto. simpl in |- *; auto. rewrite app_nil_r; auto. rewrite app_nil_r; auto. Qed.
imports: Buchberger(Buch)