proposition: Theorem buch_spolyQ : forall P : list (poly A0 eqA ltM), SpolyQ A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec (buch P).
proof: Proof. intros P. apply reds_SpolyQ1; auto. intros; apply buch_reds; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)