proposition: Theorem Cb_Red : forall (L : list (poly A0 eqA ltM)) (p : poly A0 eqA ltM), In p L -> Cb A A0 eqA plusA multA eqA_dec n ltM ltM_dec p (Red L).
proof: Proof. intros L p H'. lapply (cb_redacc L nil p); [ intros H'3; generalize H'3 | idtac ]; simpl in |- *; auto. rewrite app_nil_r; auto. Qed.
imports: Buchberger(Buch)