proposition: Theorem slice_Tl : forall (a ia : poly A0 eqA ltM) (L : list (poly A0 eqA ltM)), Tl (slicef a ia L) (a :: L).
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); unfold Tl in |- *; simpl in |- *; auto. intros c l. unfold slicef in |- *; simpl in |- *; auto. case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a b) c); auto. unfold Tl in |- *; simpl in |- *; auto. case (divp_dec _ _ _ _ _ _ _ _ _ cs n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a c) b); auto. intros H' H'0; case (slice a b l); simpl in |- *; auto. unfold Tl in |- *; simpl in |- *; auto. unfold Tl in |- *; simpl in |- *; auto. unfold Tl in |- *; intros H' H'0; case (slice a b l); simpl in |- *; auto with arith. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)