proposition: Theorem redbuch_Grobner : forall P : list (poly A0 eqA ltM), Grobner A A0 A1 eqA plusA invA minusA multA divA eqA_dec n ltM ltM_dec (redbuch P).
proof: Proof. intros P. unfold redbuch in |- *. apply Red_grobner; auto. apply buch_Grobner; auto. Qed.
imports: Buchberger(Buch)