proposition: Theorem ObuchPincl : forall aP R Q : list (poly A0 eqA ltM), OBuch aP Q R -> incl aP R.
proof: Proof. intros aP R Q H'; elim H'; simpl in |- *; auto. intros a aP0 Q0 R0 H'0 H'1 H'2; try assumption. apply incl_tran with (m := nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a aP0 :: aP0); simpl in |- *; auto. apply incl_addEnd1; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)