proposition: Theorem OBuch_Inv_f : forall P Q : list (poly A0 eqA ltM), OBuch P (genOCPf P) Q -> forall a b : poly A0 eqA ltM, In a Q -> In b Q -> reds a b Q.
proof: Proof. intros P Q H' a b H'0 H'1; try assumption. apply OBuch_Inv with (aP := P) (Q := genOCPf P); auto. intros a0 b0 H'3 H'4. apply genOCp_redln; auto. apply ObuchPincl with (Q := genOCPf P); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)