proposition: Theorem slice_inv : forall (a b : poly A0 eqA ltM) (P : list (poly A0 eqA ltM)) (c : poly A0 eqA ltM), In c P -> In c (getRes (slice a b P)) \/ divp A A0 eqA multA divA n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a c) b.
proof: Proof. intros a b P; elim P; simpl in |- *; auto. intros c H'; elim H'. intros p aP1; case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a b) p); simpl in |- *; auto. case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a p) b); auto. intros H' H'0 H'1 c H'2; elim H'2; [ intros H'3; rewrite <- H'3; clear H'2 | intros H'3; clear H'2 ]; auto. case (slice a b aP1); simpl in |- *; auto. intros P0 H' H'0 H'1 c H'2; elim H'2; [ intros H'3; rewrite <- H'3; clear H'2 | intros H'3; clear H'2 ]; auto. elim (H'1 c); [ intros H'5; try exact H'5 | intros H'5 | idtac ]; auto. intros P0 H' H'0 H'1 c H'2; elim H'2; [ intros H'3; rewrite <- H'3; clear H'2 | intros H'3; clear H'2 ]; auto. elim (H'1 c); [ intros H'5; try exact H'5 | intros H'5 | idtac ]; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)