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