proposition: Theorem pbuchf_Stable : forall P R : list (poly A0 eqA ltM), R = strip _ (pbuchf (P, genOCPf P)) -> stable P R.
proof: Proof. simpl in |- *. intros P R H'; try assumption. apply OBuch_Stable_f; auto. rewrite H'. case (pbuchf (pair P (genOCPf P))); simpl in |- *; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)