proposition: Theorem buch_Grobner : forall P : list (poly A0 eqA ltM), Grobner A A0 A1 eqA plusA invA minusA multA divA eqA_dec n ltM ltM_dec (buch P).
proof: Proof. intros P. apply ConfluentReduce_imp_Grobner; auto. apply SpolyQ_imp_ConfluentReduce with (1 := cs); auto. apply buch_spolyQ; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)