proposition: Theorem cb_redacc : forall (L1 L2 : list poly) (p : poly), In p L1 -> cb (redacc L1 L2 ++ L2) p.
proof: Proof. intros L1; elim L1; simpl in |- *; auto. intros L2 p H'; elim H'; auto. unfold LetP in |- *. intros a l H' L2 p H'0; case H'0; [ intros H'1; rewrite H'1; clear H'0 | intros H'1; clear H'0 ]; auto. case (zerop_dec (nf (l ++ L2) p)); auto. intros H'0. apply cb_comp with (L1 := l ++ L2); auto. intros p0 H'2. lapply (in_app_or l L2 p0); auto. intros H'3; case H'3; auto. intros H'0. 2: case (zerop_dec (nf (l ++ L2) a)); auto. 2: intros H'0. 2: apply cb_incl with (L1 := redacc l (nf (l ++ L2) a :: L2) ++ nf (l ++ L2) a :: L2); auto with datatypes. apply cb_compo with (L1 := nf (l ++ L2) p :: l ++ L2); simpl in |- *; auto. intros q H'2; case H'2; [ intros H'3; rewrite <- H'3; clear H'2 | intros H'3; clear H'2 ]; auto with datatypes. case (in_app_or l L2 q H'3); auto with datatypes. intros H'2. apply cb_incl with (L1 := redacc l (nf (l ++ L2) p :: L2) ++ nf (l ++ L2) p :: L2); auto with datatypes. Qed.
imports: Coq(List Relation_Definitions) Buchberger(LetP)