proposition: Theorem ObuchQred : forall aP R Q : list (poly A0 eqA ltM), OBuch aP Q R -> forall a : poly A0 eqA ltM, In a Q -> 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 aL a H'0; elim H'0. intros a aP0 Q0 R0 H'0 H'1 H'2 a0 H'3; elim H'3; [ intros H'4; rewrite <- H'4; clear H'3 | intros H'4; clear H'3 ]; auto. apply red_incl with (1 := cs) (p := addEnd A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a aP0) aP0); auto. apply ObuchPincl with (Q := genPcPf (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a aP0) aP0 Q0); auto. apply nf_red with (cs := cs) (os := os) (aP := aP0); simpl in |- *; auto. unfold incl in |- *; auto. apply red_cons with (1 := cs); auto. apply H'1; auto. apply (genPcPf_incl (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a aP0) aP0 Q0); auto. intros a aP0 Q0 R0 H'0 H'1 H'2 a0 H'3; elim H'3; [ intros H'4; rewrite <- H'4; clear H'3 | intros H'4; clear H'3 ]; auto. apply red_incl with (1 := cs) (p := aP0); auto. apply ObuchPincl with (Q := Q0); auto. apply zerop_red with (cs := cs) (os := os); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)