proposition: Theorem reds_SpolyQ1 : forall P : list (poly A0 eqA ltM), (forall a b : poly A0 eqA ltM, In a P -> In b P -> reds a b P) -> SpolyQ A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec P.
proof: Proof. intros P H'. apply SpolyQ0; auto. intros p q H'0 H'1 H'2 H'3. elim (imp_in P p); [ intros b E; elim E; intros H'7 H'8; clear E | idtac ]; auto. rewrite H'8. elim (imp_in P q); [ intros b0 E; elim E; intros H'9 H'10; clear E | idtac ]; auto. rewrite H'10. apply reds_SpolyQ; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)