proposition: Theorem buch_Stable : forall P : list (poly A0 eqA ltM), stable P (buch P).
proof: Proof. intros P; apply pbuchf_Stable; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)