proposition: Theorem redbuch_stable : forall P : list (poly A0 eqA ltM), stable A A0 eqA plusA multA eqA_dec n ltM ltM_dec P (redbuch P).
proof: Proof. intros P. cut (stable A A0 eqA plusA multA eqA_dec n ltM ltM_dec P (buch A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os P)). intros H'0; inversion H'0; auto. apply stable0; unfold redbuch in |- *; auto. intros a H'. apply cb_Red_cb1; auto. intros a H'. apply H0; auto. apply cb_Red_cb2; auto. apply buch_Stable; auto. Qed.
imports: Buchberger(Buch)