proposition: Theorem OBuch_Stable_f : forall P Q : list (poly A0 eqA ltM), OBuch P (genOCPf P) Q -> stable P Q.
proof: Proof. intros P Q H'; try assumption. apply OBuch_Stable with (Q := genOCPf P); auto. intros a H'0; try assumption. apply genOCPf_stable; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)