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