proposition: Theorem pbuchf_Inv : forall P R : list (poly A0 eqA ltM), R = strip _ (pbuchf (P, genOCPf P)) -> forall a b : poly A0 eqA ltM, In a R -> In b R -> reds a b R.
proof: Proof. intros P R H' a b H'0 H'1; simpl in |- *. apply OBuch_Inv_f with (P := P); auto. rewrite H'; simpl in |- *; auto. case (pbuchf (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)