proposition: Theorem ObuchPred : forall aP R Q : list (poly A0 eqA ltM), OBuch aP Q R -> forall a : poly A0 eqA ltM, In a aP -> red A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a R.
proof: Proof. intros aP R Q H'; elim H'; simpl in |- *; auto. intros; apply red_cons with (1 := cs); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)