proposition: Remark lem_redln_cons_gen : forall (aP R Q : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), In a aP -> In b aP -> redIn a b aP Q R -> forall (c : poly A0 eqA ltM) (Q1 : list (poly A0 eqA ltM)), incl (addEnd A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os c aP) aP) R -> Q = c :: Q1 -> redIn a b (addEnd A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os c aP) aP) Q1 R.
proof: Proof. intros aP R Q a b H' H'0 H'1; elim H'1; auto. intros P Q0 R0 a0 b0 H'2 H'3 c Q1 H'4 H'5. apply redIn0b; auto. intros P Q0 R0 a0 b0 H'2 c Q1 H'3 H'4. rewrite H'4 in H'2; elim H'2; auto. intros H'5; rewrite H'5. apply redIn1; auto. apply nf_red with (aP := P) (cs := cs) (os := os); auto. apply incl_tran with (m := nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os c P :: P); simpl in |- *; auto. apply incl_addEnd1; auto. apply red_cons with (1 := cs); auto. apply in_incl with (p := nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os c P :: P); auto. apply incl_addEnd1; auto. rewrite H'5; simpl in |- *; auto. intros P Q0 R0 a0 b0 c H'2 H'3 H'4 H'5 H'6 H'7 c0 Q1 H'8 H'9. apply redIn2 with (c := c); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)