proposition: Theorem genOCp_redln : forall aL1 R : list (poly A0 eqA ltM), incl aL1 R -> forall a b : poly A0 eqA ltM, In a aL1 -> In b aL1 -> redIn a b aL1 (genOCPf aL1) R.
proof: Proof. intros aL1; elim aL1; simpl in |- *; auto. intros a l H' R H'0 a0 b H'1 H'2. elim H'2; [ intros H'3; rewrite <- H'3; clear H'2 | intros H'3; clear H'2 ]; auto. elim H'1; [ intros H'2; rewrite <- H'2; clear H'1 | intros H'2; clear H'1 ]; auto. apply redIn1; auto. apply red_id; auto. apply redIn0b. case (zerop_dec A A0 eqA n ltM a); intros Z; auto. apply redIn1; auto. apply zerop_red_spoly_l; auto. case (zerop_dec A A0 eqA n ltM a0); intros Z1; auto. apply redIn1; auto. apply zerop_red_spoly_r; auto. lapply (spolyp_addEnd_genPcPf l); [ intros H'4; elim (H'4 (genOCPf l) a a0); [ intros c E; elim E; intros H'11 H'12; elim H'12; intros H'13 H'14; elim H'13; [ intros H'15; clear H'13 H'12 E | intros H'15; clear H'13 H'12 E ] | idtac | idtac | idtac ] | idtac ]; auto. apply redIn2 with (c := c); auto. simpl in |- *; auto. apply redInInclQ with (Q := genOCPf l); auto. apply redInclP with (P := l); auto. apply H'; auto. apply incl_tran with (m := a :: l); simpl in |- *; auto. apply redIn2 with (c := c); auto. simpl in |- *; auto. apply redIn1; auto. apply red_incl with (p := addEnd A A0 eqA n ltM a l) (1 := cs); auto. apply addEnd_incl; auto. apply redInclP with (P := l); auto. apply redInInclQ with (Q := genOCPf l); auto. apply H'; auto. apply incl_tran with (m := a :: l); auto. elim H'1; [ intros H'2; rewrite <- H'2; clear H'1 | intros H'2; clear H'1 ]; auto. case (zerop_dec A A0 eqA n ltM a); intros Z; auto. apply redIn1; auto. apply zerop_red_spoly_l; auto. case (zerop_dec A A0 eqA n ltM b); intros Z1; auto. apply redIn1; auto. apply zerop_red_spoly_r; auto. lapply (spolyp_addEnd_genPcPf l); [ intros H'4; elim (H'4 (genOCPf l) a b); [ intros c E; elim E; intros H'11 H'12; elim H'12; intros H'13 H'14; elim H'13; [ intros H'15; clear H'13 H'12 E | intros H'15; clear H'13 H'12 E ] | idtac | idtac | idtac ] | idtac ]; auto. apply redIn2 with (c := c); simpl in |- *; auto. apply redInInclQ with (Q := genOCPf l); auto. apply redInclP with (P := l); auto. apply H'; auto. apply incl_tran with (m := a :: l); simpl in |- *; auto. apply redIn2 with (c := c); simpl in |- *; auto. apply redIn1; auto. apply red_incl with (1 := cs) (p := addEnd A A0 eqA n ltM a l); auto. apply addEnd_incl; auto. apply redInclP with (P := l); auto. apply redInInclQ with (Q := genOCPf l); auto. apply H'; auto. apply incl_tran with (m := a :: l); auto. apply redInclP with (P := l); auto. apply redInInclQ with (Q := genOCPf l); auto. apply H'; auto. apply incl_tran with (m := a :: l); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)