proposition: Theorem red_divp : forall (L : list poly) (p : poly), In p L -> ~ zerop p -> exists q : poly, In q (red L) /\ divp p q /\ ~ zerop 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: Coq(List Relation_Definitions) Buchberger(LetP)