proposition: Theorem Red_grobner : forall L : list (poly A0 eqA ltM), Grobner A A0 A1 eqA plusA invA minusA multA divA eqA_dec n ltM ltM_dec L -> Grobner A A0 A1 eqA plusA invA minusA multA divA eqA_dec n ltM ltM_dec (Red L).
proof: Proof. intros L H'. apply def_grobner; auto. intros p H'0. lapply (grobner_def L); [ intros H'2; lapply (H'2 p); [ intros H'4 | idtac ] | idtac ]; auto. case H'4; auto. intros H'1; case H'1; intros q E; clear H'1. right. apply divp_reduce1 with (L1 := L) (q := q); auto. intros r1 H'1 H'3. lapply (Red_divp L r1); [ intros H'7; lapply H'7; [ intros H'8; clear H'7 | clear H'7 ] | idtac ]; auto. case H'8; intros q0 E0; case E0; intros H'5 H'6; case H'6; intros H'7 H'9; clear H'6 E0 H'8. exists q0; split; auto. apply cb_Red_cb2; auto. Qed.
imports: Buchberger(Buch)