proposition: Remark lem_redIn_nil : forall (aP Q R : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), In a R -> In b R -> redIn a b aP Q R -> Q = nil -> aP = R -> reds a b R.
proof: Proof. intros aP Q R a b H' H'0 H'1; elim H'1; auto. intros P Q0 R0 a0 b0 H'2 H'3 H'4 H'5. apply reds_com; auto. intros P Q0 R0 a0 b0 H'2 H'3 H'4. rewrite H'3 in H'2; elim H'2. intros P Q0 R0 a0 b0 H'2 H'3 H'4; rewrite <- H'4. rewrite H'4. apply reds0; auto. intros P Q0 R0 a0 b0 c H'2 H'3 H'4 H'5 H'6 H'7 H'8 H'9. apply reds1 with (c := c); auto. rewrite <- H'9; auto. apply reds_com; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)