proposition: Theorem OBuch_Inv : forall aP R Q : list (poly A0 eqA ltM), OBuch aP Q R -> (forall a b : poly A0 eqA ltM, In a aP -> In b aP -> redIn a b aP Q R) -> forall a b : poly A0 eqA ltM, In a R -> In b R -> reds a b R.
proof: Proof. intros aP R Q H'; elim H'; simpl in |- *; auto. intros aL H'0 a b H'1 H'2; try assumption. apply redIn_nil; auto. intros a aP0 Q0 R0 H'0 H'1 H'2 H'3 a0 b H'4 H'5. apply H'1; auto. intros a1 b0 H'6. case (addEnd_cons A A0 eqA n ltM) with (1 := H'6); auto. intros H'7; rewrite <- H'7; auto. intros H'8. case (addEnd_cons A A0 eqA n ltM) with (1 := H'8); auto. intros H'9; rewrite <- H'9; auto. apply redIn1; auto. apply red_id; auto. intros H'9. case (zerop_dec A A0 eqA n ltM b0); intros Z; auto. apply redIn1; auto. apply zerop_red_spoly_r; auto. rewrite H'7; auto. apply red_gen_in; auto. intros H'7 H'8. case (addEnd_cons A A0 eqA n ltM) with (1 := H'8); auto. intros H'9; rewrite <- H'9; auto. apply redIn0b. case (zerop_dec A A0 eqA n ltM a1); intros Z. apply redIn1; auto. apply zerop_red_spoly_r; auto. rewrite H'9. apply red_gen_in; auto. intros H'9. apply redln_cons with (c := a); simpl in |- *; auto. apply redInclP with (P := aP0); auto. apply redInInclQ with (Q := a :: Q0); auto with datatypes. unfold incl in |- *; auto. apply nf_red with (aP := aP0) (cs := cs) (os := os); auto. apply incl_tran with (m := 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. unfold incl in |- *; 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 red_cons with (1 := cs); auto. apply in_incl with (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); simpl in |- *; 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. intros a aP0 Q0 R0 H'0 H'1 H'2 H'3 a0 b H'4 H'5. apply H'1; auto. intros a1 b0 H'6 H'7. apply redln_cons with (c := a); auto. apply red_incl with (p := aP0) (1 := cs); 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)