proposition: Theorem redacc_divp : forall (L1 L2 : list poly) (p : poly), ~ zerop p -> In p (L1 ++ L2) -> exists q : poly, In q (redacc L1 L2 ++ L2) /\ divp p q /\ ~ zerop q.
proof: Proof. intros L1; elim L1; simpl in |- *; auto. intros L2 p H' H'0; exists p; split; auto. unfold LetP in |- *. intros a l H' L2 p H'0 H'1; case H'1; [ intros H'2; rewrite <- H'2; clear H'1 | intros H'2; clear H'1 ]; auto. case (zerop_dec (nf (l ++ L2) a)); simpl in |- *; auto. intros Z1. lapply (nf_div_zero1 a (l ++ L2)); [ intros H'5; lapply H'5; [ intros H'6; clear H'5 | clear H'5 ] | idtac ]; auto. case H'6; intros q E; case E; intros H'3 H'4; case H'4; intros H'5 H'7; clear H'4 E H'6. lapply (H' L2 q); [ intros H'8; lapply H'8; [ intros H'9; clear H'8 | clear H'8 ] | idtac ]; auto. case H'9; intros q0 E; case E; intros H'4 H'6; case H'6; intros H'8 H'10; clear H'6 E H'9. exists q0; split; [ idtac | split ]; auto. apply divp_trans with (y := q); auto. rewrite H'2; auto. intros Z1. lapply (nf_div a (l ++ L2)); [ intros H'5; lapply H'5; [ intros H'6; clear H'5 | clear H'5 ] | idtac ]; auto. case H'6; intros q E; case E; intros H'3 H'4; case H'4; intros H'5 H'7; clear H'4 E H'6. simpl in H'3. case H'3; [ intros H'4; clear H'3 | intros H'4; clear H'3 ]. exists q; split; [ idtac | split ]; auto. lapply (H' (nf (l ++ L2) a :: L2) q); [ intros H'8; lapply H'8; [ intros H'9; clear H'8 | clear H'8 ] | idtac ]; auto. case H'9; intros q0 E; case E; intros H'3 H'6; case H'6; intros H'8 H'10; clear H'6 E H'9. exists q0; split; [ idtac | split ]; auto. case (in_app_or (redacc l (nf (l ++ L2) a :: L2)) (nf (l ++ L2) a :: L2) q0 H'3); auto. simpl in |- *; auto. intros H'6; case H'6; [ intros H'9; clear H'6 | intros H'9; clear H'6 ]; auto. apply divp_trans with (y := q); auto. case (in_app_or l L2 q H'4); auto with datatypes. rewrite H'2; auto. case (zerop_dec (nf (l ++ L2) a)); simpl in |- *; auto. intros Z1. case (in_app_or l L2 p H'2); auto. intros H'3. lapply (H' (nf (l ++ L2) a :: L2) p); [ intros H'6; lapply H'6; [ intros H'7; clear H'6 | clear H'6 ] | idtac ]; auto. case H'7; intros q E; case E; intros H'4 H'5; case H'5; intros H'6 H'8; clear H'5 E H'7. exists q; split; auto. case (in_app_or (redacc l (nf (l ++ L2) a :: L2)) (nf (l ++ L2) a :: L2) q H'4); auto. simpl in |- *; auto. intros H; case H; intros H1; auto. intros H; exists p; split; [ right | idtac ]; auto. Qed.
imports: Coq(List Relation_Definitions) Buchberger(LetP)