proposition: Theorem slicef_incl : forall (a b : poly A0 eqA ltM) (P : list (poly A0 eqA ltM)), incl (slicef a b P) P.
proof: Proof. intros a b P; elim P; simpl in |- *; auto. unfold slicef in |- *; simpl in |- *; auto. case (foreigner_dec A A0 A1 eqA multA n ltM a b); intros H; apply incl_refl; auto with datatypes. intros c; unfold slicef in |- *; simpl in |- *. case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a b) c); auto with datatypes. case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a c) b); auto with datatypes. intros H' H'0 l; case (slice a b l); simpl in |- *; auto with datatypes. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)