proposition: Theorem buch_reds : forall (P : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), In a (buch P) -> In b (buch P) -> reds a b (buch P).
proof: Proof. intros P a b H' H'0. apply pbuchf_Inv with (P := P); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)