proposition: Theorem slice_cons : forall (i a : poly A0 eqA ltM) (aP Q : list (poly A0 eqA ltM)), slice i a aP = DontKeep Q -> (exists c : poly A0 eqA ltM, In c Q /\ divp A A0 eqA multA divA n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i a) c) \/ foreigner A A0 A1 eqA multA n ltM i a.
proof: Proof. intros i a aP; elim aP. simpl in |- *; case (foreigner_dec A A0 A1 eqA multA n ltM i a); auto. intros H' Q H'0; inversion H'0. intros a0 l H' Q; simpl in |- *. case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i a) a0); auto. intros H'0 H'1; inversion H'1; auto. left; exists a0; split; simpl in |- *; auto. case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i a0) a); auto. generalize H'; clear H'; case (slice i a l); simpl in |- *; auto. intros P H' H'0 H'1 H'2; inversion H'2. intros P H' H'0 H'1 H'2; inversion H'2. elim (H' P); [ intros H'5; elim H'5; intros c E; elim E; intros H'6 H'7; clear E H'5 | intros H'5 | idtac ]; auto. left; exists c; split; simpl in |- *; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)