proposition: Remark lem_redln_cons : 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)), Q = c :: Q1 -> red A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec c R -> redIn a b 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. apply H'3 with (c := c); auto. intros P Q0 R0 a0 b0 H'2 c Q1 H'3 H'4. rewrite H'3 in H'2; elim H'2; auto. intros H'5; rewrite H'5 in H'4; 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. apply (H'4 c0); auto. apply (H'6 c0); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)