Update build process to use COQPATH & _CoqProject

Removed all of the files not built by default; they can be resurrected from git
history.  _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile.  COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).

5 files changed, 0 insertions, 1347 deletions

diff --git a/coqprime/List/Iterator.v b/coqprime/List/Iterator.v
deleted file mode 100644
index 96d3e5655..000000000
--- a/coqprime/List/Iterator.v
+++ /dev/null
@@ -1,180 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-Require Export List.
-Require Export Permutation.
-Require Import Arith.
- 
-Section Iterator.
-Variables A B : Set.
-Variable zero : B.
-Variable f : A ->  B.
-Variable g : B -> B ->  B.
-Hypothesis g_zero : forall a,  g a zero = a.
-Hypothesis g_trans : forall a b c,  g a (g b c) = g (g a b) c.
-Hypothesis g_sym : forall a b,  g a b = g b a.
- 
-Definition iter := fold_right (fun a r => g (f a) r) zero.
-Hint Unfold iter .
- 
-Theorem iter_app: forall l1 l2,  iter (app l1 l2) = g (iter l1) (iter l2).
-intros l1; elim l1; simpl; auto.
-intros l2; rewrite g_sym; auto.
-intros a l H l2; rewrite H.
-rewrite g_trans; auto.
-Qed.
- 
-Theorem iter_permutation: forall l1 l2, permutation l1 l2 ->  iter l1 = iter l2.
-intros l1 l2 H; elim H; simpl; auto; clear H l1 l2.
-intros a l1 l2 H1 H2; apply f_equal2 with ( f := g ); auto.
-intros a b l; (repeat rewrite g_trans).
-apply f_equal2 with ( f := g ); auto.
-intros l1 l2 l3 H H0 H1 H2; apply trans_equal with ( 1 := H0 ); auto.
-Qed.
- 
-Lemma iter_inv:
- forall P l,
- P zero ->
- (forall a b, P a -> P b ->  P (g a b)) ->
- (forall x, In x l ->  P (f x)) ->  P (iter l).
-intros P l H H0; (elim l; simpl; auto).
-Qed.
-Variable next : A ->  A.
- 
-Fixpoint progression (m : A) (n : nat) {struct n} : list A :=
- match n with   0 => nil
-               | S n1 => cons m (progression (next m) n1) end.
- 
-Fixpoint next_n (c : A) (n : nat) {struct n} : A :=
- match n with 0 => c | S n1 => next_n (next c) n1 end.
- 
-Theorem progression_app:
- forall a b n m,
- le m n ->
- b = next_n a m ->
-  progression a n = app (progression a m) (progression b (n - m)).
-intros a b n m; generalize a b n; clear a b n; elim m; clear m; simpl.
-intros a b n H H0; apply f_equal2 with ( f := progression ); auto with arith.
-intros m H a b n; case n; simpl; clear n.
-intros H1; absurd (0 < 1 + m); auto with arith.
-intros n H0 H1; apply f_equal2 with ( f := @cons A ); auto with arith.
-Qed.
- 
-Let iter_progression := fun m n => iter (progression m n).
- 
-Theorem iter_progression_app:
- forall a b n m,
- le m n ->
- b = next_n a m ->
-  iter (progression a n) =
-  g (iter (progression a m)) (iter (progression b (n - m))).
-intros a b n m H H0; unfold iter_progression; rewrite (progression_app a b n m);
- (try apply iter_app); auto.
-Qed.
- 
-Theorem length_progression: forall z n,  length (progression z n) = n.
-intros z n; generalize z; elim n; simpl; auto.
-Qed.
- 
-End Iterator.
-Implicit Arguments iter [A B].
-Implicit Arguments progression [A].
-Implicit Arguments next_n [A].
-Hint Unfold iter .
-Hint Unfold progression .
-Hint Unfold next_n .
- 
-Theorem iter_ext:
- forall (A B : Set) zero (f1 : A ->  B) f2 g l,
- (forall a, In a l ->  f1 a = f2 a) ->  iter zero f1 g l = iter zero f2 g l.
-intros A B zero f1 f2 g l; elim l; simpl; auto.
-intros a l0 H H0; apply f_equal2 with ( f := g ); auto.
-Qed.
- 
-Theorem iter_map:
- forall (A B C : Set) zero (f : B ->  C) g (k : A ->  B) l,
-  iter zero f g (map k l) = iter zero (fun x => f (k x)) g l.
-intros A B C zero f g k l; elim l; simpl; auto.
-intros; apply f_equal2 with ( f := g ); auto with arith.
-Qed.
- 
-Theorem iter_comp:
- forall (A B : Set) zero (f1 f2 : A ->  B) g l,
- (forall a,  g a zero = a) ->
- (forall a b c,  g a (g b c) = g (g a b) c) ->
- (forall a b,  g a b = g b a) ->
-  g (iter zero f1 g l) (iter zero f2 g l) =
-  iter zero (fun x => g (f1 x) (f2 x)) g l.
-intros A B zero f1 f2 g l g_zero g_trans g_sym; elim l; simpl; auto.
-intros a l0 H; rewrite <- H; (repeat rewrite <- g_trans).
-apply f_equal2 with ( f := g ); auto.
-(repeat rewrite g_trans); apply f_equal2 with ( f := g ); auto.
-Qed.
- 
-Theorem iter_com:
- forall (A B : Set) zero (f : A -> A ->  B) g l1 l2,
- (forall a,  g a zero = a) ->
- (forall a b c,  g a (g b c) = g (g a b) c) ->
- (forall a b,  g a b = g b a) ->
-  iter zero (fun x => iter zero (fun y => f x y) g l1) g l2 =
-  iter zero (fun y => iter zero (fun x => f x y) g l2) g l1.
-intros A B zero f g l1 l2 H H0 H1; generalize l2; elim l1; simpl; auto;
- clear l1 l2.
-intros l2; elim l2; simpl; auto with arith.
-intros; rewrite H1; rewrite H; auto with arith.
-intros a l1 H2 l2; case l2; clear l2; simpl; auto.
-elim l1; simpl; auto with arith.
-intros; rewrite H1; rewrite H; auto with arith.
-intros b l2.
-rewrite <- (iter_comp
-             _ _ zero (fun x => f x a)
-             (fun x => iter zero (fun (y : A) => f x y) g l1)); auto with arith.
-rewrite <- (iter_comp
-             _ _ zero (fun y => f b y)
-             (fun y => iter zero (fun (x : A) => f x y) g l2)); auto with arith.
-(repeat rewrite H0); auto.
-apply f_equal2 with ( f := g ); auto.
-(repeat rewrite <- H0); auto.
-apply f_equal2 with ( f := g ); auto.
-Qed.
- 
-Theorem iter_comp_const:
- forall (A B : Set) zero (f : A ->  B) g k l,
- k zero = zero ->
- (forall a b,  k (g a b) = g (k a) (k b)) ->
-  k (iter zero f g l) = iter zero (fun x => k (f x)) g l.
-intros A B zero f g k l H H0; elim l; simpl; auto.
-intros a l0 H1; rewrite H0; apply f_equal2 with ( f := g ); auto.
-Qed.
- 
-Lemma next_n_S: forall n m,  next_n S n m = plus n m.
-intros n m; generalize n; elim m; clear n m; simpl; auto with arith.
-intros m H n; case n; simpl; auto with arith.
-rewrite H; auto with arith.
-intros n1; rewrite H; simpl; auto with arith.
-Qed.
- 
-Theorem progression_S_le_init:
- forall n m p, In p (progression S n m) ->  le n p.
-intros n m; generalize n; elim m; clear n m; simpl; auto.
-intros; contradiction.
-intros m H n p [H1|H1]; auto with arith.
-subst n; auto.
-apply le_S_n; auto with arith.
-Qed.
- 
-Theorem progression_S_le_end:
- forall n m p, In p (progression S n m) ->  lt p (n + m).
-intros n m; generalize n; elim m; clear n m; simpl; auto.
-intros; contradiction.
-intros m H n p [H1|H1]; auto with arith.
-subst n; auto with arith.
-rewrite <- plus_n_Sm; auto with arith.
-rewrite <- plus_n_Sm; auto with arith.
-generalize (H (S n) p); auto with arith.
-Qed.
diff --git a/coqprime/List/ListAux.v b/coqprime/List/ListAux.v
deleted file mode 100644
index c3c9602bd..000000000
--- a/coqprime/List/ListAux.v
+++ /dev/null
@@ -1,271 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-(**********************************************************************
-     Aux.v                                                                                           
-                                                                                                          
-     Auxillary functions & Theorems                                              
-  **********************************************************************)
-Require Export List.
-Require Export Arith.
-Require Export Tactic.
-Require Import Inverse_Image.
-Require Import Wf_nat.
-
-(************************************** 
-   Some properties on list operators: app, map,...
-**************************************)
- 
-Section List.
-Variables (A : Set) (B : Set) (C : Set).
-Variable f : A ->  B.
-
-(************************************** 
-  An induction theorem for list based on length 
-**************************************)
- 
-Theorem list_length_ind:
- forall (P : list A ->  Prop),
- (forall (l1 : list A),
-  (forall (l2 : list A), length l2 < length l1 ->  P l2) ->  P l1) ->
- forall (l : list A),  P l.
-intros P H l;
- apply well_founded_ind with ( R := fun (x y : list A) => length x < length y );
- auto.
-apply wf_inverse_image with ( R := lt ); auto.
-apply lt_wf.
-Qed.
- 
-Definition list_length_induction:
- forall (P : list A ->  Set),
- (forall (l1 : list A),
-  (forall (l2 : list A), length l2 < length l1 ->  P l2) ->  P l1) ->
- forall (l : list A),  P l.
-intros P H l;
- apply well_founded_induction
-      with ( R := fun (x y : list A) => length x < length y ); auto.
-apply wf_inverse_image with ( R := lt ); auto.
-apply lt_wf.
-Qed.
- 
-Theorem in_ex_app:
- forall (a : A) (l : list A),
- In a l ->  (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2)  ).
-intros a l; elim l; clear l; simpl; auto.
-intros H; case H.
-intros a1 l H [H1|H1]; auto.
-exists (nil (A:=A)); exists l; simpl; auto.
-rewrite H1; auto.
-case H; auto; intros l1 [l2 Hl2]; exists (a1 :: l1); exists l2; simpl; auto.
-rewrite Hl2; auto.
-Qed.
-
-(**************************************
- Properties on app 
-**************************************)
- 
-Theorem length_app:
- forall (l1 l2 : list A),  length (l1 ++ l2) = length l1 + length l2.
-intros l1; elim l1; simpl; auto.
-Qed.
- 
-Theorem app_inv_head:
- forall (l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3 ->  l2 = l3.
-intros l1; elim l1; simpl; auto.
-intros a l H l2 l3 H0; apply H; injection H0; auto.
-Qed.
- 
-Theorem app_inv_tail:
- forall (l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1 ->  l2 = l3.
-intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto.
-intros l1 l3; case l3; auto.
-intros b l H; absurd (length ((b :: l) ++ l1) <= length l1).
-simpl; rewrite length_app; auto with arith.
-rewrite <- H; auto with arith.
-intros a l H l1 l3; case l3.
-simpl; intros H1; absurd (length (a :: (l ++ l1)) <= length l1).
-simpl; rewrite length_app; auto with arith.
-rewrite H1; auto with arith.
-simpl; intros b l0 H0; injection H0.
-intros H1 H2; rewrite H2, (H _ _ H1); auto.
-Qed.
- 
-Theorem app_inv_app:
- forall l1 l2 l3 l4 a,
- l1 ++ l2 = l3 ++ (a :: l4) ->
-  (exists l5 : list A , l1 = l3 ++ (a :: l5) ) \/
-  (exists l5 , l2 = l5 ++ (a :: l4) ).
-intros l1; elim l1; simpl; auto.
-intros l2 l3 l4 a H; right; exists l3; auto.
-intros a l H l2 l3 l4 a0; case l3; simpl.
-intros H0; left; exists l; injection H0; intros; subst; auto.
-intros b l0 H0; case (H l2 l0 l4 a0); auto.
-injection H0; auto.
-intros [l5 H1].
-left; exists l5; injection H0; intros; subst; auto.
-Qed.
- 
-Theorem app_inv_app2:
- forall l1 l2 l3 l4 a b,
- l1 ++ l2 = l3 ++ (a :: (b :: l4)) ->
-  (exists l5 : list A , l1 = l3 ++ (a :: (b :: l5)) ) \/
-  ((exists l5 , l2 = l5 ++ (a :: (b :: l4)) ) \/
-   l1 = l3 ++ (a :: nil) /\ l2 = b :: l4).
-intros l1; elim l1; simpl; auto.
-intros l2 l3 l4 a b H; right; left; exists l3; auto.
-intros a l H l2 l3 l4 a0 b; case l3; simpl.
-case l; simpl.
-intros H0; right; right; injection H0; split; auto.
-rewrite H2; auto.
-intros b0 l0 H0; left; exists l0; injection H0; intros; subst; auto.
-intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto.
-injection H0; auto.
-intros [l5 HH1]; left; exists l5; injection H0; intros; subst; auto.
-intros [H1|[H1 H2]]; auto.
-right; right; split; auto; injection H0; intros; subst; auto.
-Qed.
- 
-Theorem same_length_ex:
- forall (a : A) l1 l2 l3,
- length (l1 ++ (a :: l2)) = length l3 ->
-  (exists l4 ,
-   exists l5 ,
-   exists b : B ,
-   length l1 = length l4 /\ (length l2 = length l5 /\ l3 = l4 ++ (b :: l5))   ).
-intros a l1; elim l1; simpl; auto.
-intros l2 l3; case l3; simpl; (try (intros; discriminate)).
-intros b l H; exists (nil (A:=B)); exists l; exists b; (repeat (split; auto)).
-intros a0 l H l2 l3; case l3; simpl; (try (intros; discriminate)).
-intros b l0 H0.
-case (H l2 l0); auto.
-intros l4 [l5 [b1 [HH1 [HH2 HH3]]]].
-exists (b :: l4); exists l5; exists b1; (repeat (simpl; split; auto)).
-rewrite HH3; auto.
-Qed.
-
-(************************************** 
-  Properties on map 
-**************************************)
- 
-Theorem in_map_inv:
- forall (b : B) (l : list A),
- In b (map f l) ->  (exists a : A , In a l /\ b = f a ).
-intros b l; elim l; simpl; auto.
-intros tmp; case tmp.
-intros a0 l0 H [H1|H1]; auto.
-exists a0; auto.
-case (H H1); intros a1 [H2 H3]; exists a1; auto.
-Qed.
- 
-Theorem in_map_fst_inv:
- forall a (l : list (B * C)),
- In a (map (fst (B:=_)) l) ->  (exists c , In (a, c) l ).
-intros a l; elim l; simpl; auto.
-intros H; case H.
-intros a0 l0 H [H0|H0]; auto.
-exists (snd a0); left; rewrite <- H0; case a0; simpl; auto.
-case H; auto; intros l1 Hl1; exists l1; auto.
-Qed.
- 
-Theorem length_map: forall l,  length (map f l) = length l.
-intros l; elim l; simpl; auto.
-Qed.
- 
-Theorem map_app: forall l1 l2,  map f (l1 ++ l2) = map f l1 ++ map f l2.
-intros l; elim l; simpl; auto.
-intros a l0 H l2; rewrite H; auto.
-Qed.
- 
-Theorem map_length_decompose:
- forall l1 l2 l3 l4,
- length l1 = length l2 ->
- map f (app l1 l3) = app l2 l4 ->  map f l1 = l2 /\ map f l3 = l4.
-intros l1; elim l1; simpl; auto; clear l1.
-intros l2; case l2; simpl; auto.
-intros; discriminate.
-intros a l1 Rec l2; case l2; simpl; clear l2; auto.
-intros; discriminate.
-intros b l2 l3 l4 H1 H2.
-injection H2; clear H2; intros H2 H3.
-case (Rec l2 l3 l4); auto.
-intros H4 H5; split; auto.
-subst; auto.
-Qed.
-
-(************************************** 
-  Properties of flat_map 
-**************************************)
- 
-Theorem in_flat_map:
- forall (l : list B) (f : B ->  list C) a b,
- In a (f b) -> In b l ->  In a (flat_map f l).
-intros l g; elim l; simpl; auto.
-intros a l0 H a0 b H0 [H1|H1]; apply in_or_app; auto.
-left; rewrite H1; auto.
-right; apply H with ( b := b ); auto.
-Qed.
- 
-Theorem in_flat_map_ex:
- forall (l : list B) (f : B ->  list C) a,
- In a (flat_map f l) ->  (exists b , In b l /\ In a (f b) ).
-intros l g; elim l; simpl; auto.
-intros a H; case H.
-intros a l0 H a0 H0; case in_app_or with ( 1 := H0 ); simpl; auto.
-intros H1; exists a; auto.
-intros H1; case H with ( 1 := H1 ).
-intros b [H2 H3]; exists b; simpl; auto.
-Qed.
-
-(************************************** 
-  Properties of fold_left 
-**************************************)
-
-Theorem fold_left_invol: 
-  forall (f: A -> B -> A) (P: A -> Prop) l a,
-  P a ->  (forall x y, P x -> P (f x y)) -> P (fold_left f l a).
-intros f1 P l; elim l; simpl; auto.
-Qed. 
-
-Theorem fold_left_invol_in: 
-  forall (f: A -> B -> A) (P: A -> Prop) l a b,
-  In b l -> (forall x, P (f x b)) -> (forall x y, P x -> P (f x y)) ->
-  P (fold_left f l a).
-intros f1 P l; elim l; simpl; auto.
-intros a1 b HH; case HH.
-intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto.
-apply fold_left_invol; auto.
-apply Rec with (b := b); auto.
-Qed.
-
-End List.
-
-
-(************************************** 
-  Propertie of list_prod
-**************************************)
- 
-Theorem length_list_prod:
- forall (A : Set) (l1 l2 : list A),
-  length (list_prod l1 l2) = length l1 * length l2.
-intros A l1 l2; elim l1; simpl; auto.
-intros a l H; rewrite length_app; rewrite length_map; rewrite H; auto.
-Qed.
- 
-Theorem in_list_prod_inv:
- forall (A B : Set) a l1 l2,
- In a (list_prod l1 l2) ->
-  (exists b : A , exists c : B , a = (b, c) /\ (In b l1 /\ In c l2)  ).
-intros A B a l1 l2; elim l1; simpl; auto; clear l1.
-intros H; case H.
-intros a1 l1 H1 H2.
-case in_app_or with ( 1 := H2 ); intros H3; auto.
-case in_map_inv with ( 1 := H3 ); intros b1 [Hb1 Hb2]; auto.
-exists a1; exists b1; split; auto.
-case H1; auto; intros b1 [c1 [Hb1 [Hb2 Hb3]]].
-exists b1; exists c1; split; auto.
-Qed.
diff --git a/coqprime/List/Permutation.v b/coqprime/List/Permutation.v
deleted file mode 100644
index a06693f89..000000000
--- a/coqprime/List/Permutation.v
+++ /dev/null
@@ -1,506 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-(**********************************************************************
-    Permutation.v                        
-                                                                     
-    Defintion and properties of permutations                         
-   **********************************************************************)
-Require Export List.
-Require Export ListAux.
- 
-Section permutation.
-Variable A : Set.
-
-(************************************** 
-   Definition of permutations as sequences of adjacent transpositions
- **************************************)
- 
-Inductive permutation : list A -> list A -> Prop :=
-  | permutation_nil : permutation nil nil
-  | permutation_skip :
-      forall (a : A) (l1 l2 : list A),
-      permutation l2 l1 -> permutation (a :: l2) (a :: l1)
-  | permutation_swap :
-      forall (a b : A) (l : list A), permutation (a :: b :: l) (b :: a :: l)
-  | permutation_trans :
-      forall l1 l2 l3 : list A,
-      permutation l1 l2 -> permutation l2 l3 -> permutation l1 l3.
-Hint Constructors permutation.
-
-(************************************** 
-   Reflexivity
- **************************************)
- 
-Theorem permutation_refl : forall l : list A, permutation l l.
-simple induction l.
-apply permutation_nil.
-intros a l1 H.
-apply permutation_skip with (1 := H).
-Qed.
-Hint Resolve permutation_refl.
-
-(************************************** 
-   Symmetry
-   **************************************)
- 
-Theorem permutation_sym :
- forall l m : list A, permutation l m -> permutation m l.
-intros l1 l2 H'; elim H'.
-apply permutation_nil.
-intros a l1' l2' H1 H2.
-apply permutation_skip with (1 := H2).
-intros a b l1'.
-apply permutation_swap.
-intros l1' l2' l3' H1 H2 H3 H4.
-apply permutation_trans with (1 := H4) (2 := H2).
-Qed.
-
-(************************************** 
-   Compatibility with list length
-   **************************************)
- 
-Theorem permutation_length :
- forall l m : list A, permutation l m -> length l = length m.
-intros l m H'; elim H'; simpl in |- *; auto.
-intros l1 l2 l3 H'0 H'1 H'2 H'3.
-rewrite <- H'3; auto.
-Qed.
-
-(************************************** 
-   A permutation of the nil list is the nil list
-   **************************************)
- 
-Theorem permutation_nil_inv : forall l : list A, permutation l nil -> l = nil.
-intros l H; generalize (permutation_length _ _ H); case l; simpl in |- *;
- auto.
-intros; discriminate.
-Qed.
- 
-(************************************** 
-   A permutation of the singleton list is the singleton list
-   **************************************)
- 
-Let permutation_one_inv_aux :
-  forall l1 l2 : list A,
-  permutation l1 l2 -> forall a : A, l1 = a :: nil -> l2 = a :: nil.
-intros l1 l2 H; elim H; clear H l1 l2; auto.
-intros a l3 l4 H0 H1 b H2.
-injection H2; intros; subst; auto.
-rewrite (permutation_nil_inv _ (permutation_sym _ _ H0)); auto.
-intros; discriminate.
-Qed.
-
-Theorem permutation_one_inv :
- forall (a : A) (l : list A), permutation (a :: nil) l -> l = a :: nil.
-intros a l H; apply permutation_one_inv_aux with (l1 := a :: nil); auto.
-Qed.
-
-(************************************** 
-   Compatibility with the belonging
-   **************************************)
- 
-Theorem permutation_in :
- forall (a : A) (l m : list A), permutation l m -> In a l -> In a m.
-intros a l m H; elim H; simpl in |- *; auto; intuition.
-Qed.
-
-(************************************** 
-   Compatibility with the append function
-   **************************************)
- 
-Theorem permutation_app_comp :
- forall l1 l2 l3 l4,
- permutation l1 l2 -> permutation l3 l4 -> permutation (l1 ++ l3) (l2 ++ l4).
-intros l1 l2 l3 l4 H1; generalize l3 l4; elim H1; clear H1 l1 l2 l3 l4;
- simpl in |- *; auto.
-intros a b l l3 l4 H.
-cut (permutation (l ++ l3) (l ++ l4)); auto.
-intros; apply permutation_trans with (a :: b :: l ++ l4); auto.
-elim l; simpl in |- *; auto.
-intros l1 l2 l3 H H0 H1 H2 l4 l5 H3.
-apply permutation_trans with (l2 ++ l4); auto.
-Qed.
-Hint Resolve permutation_app_comp.
-
-(************************************** 
-   Swap two sublists
-   **************************************)
- 
-Theorem permutation_app_swap :
- forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
-intros l1; elim l1; auto.
-intros; rewrite <- app_nil_end; auto.
-intros a l H l2.
-replace (l2 ++ a :: l) with ((l2 ++ a :: nil) ++ l).
-apply permutation_trans with (l ++ l2 ++ a :: nil); auto.
-apply permutation_trans with (((a :: nil) ++ l2) ++ l); auto.
-simpl in |- *; auto.
-apply permutation_trans with (l ++ (a :: nil) ++ l2); auto.
-apply permutation_sym; auto.
-replace (l2 ++ a :: l) with ((l2 ++ a :: nil) ++ l).
-apply permutation_app_comp; auto.
-elim l2; simpl in |- *; auto.
-intros a0 l0 H0.
-apply permutation_trans with (a0 :: a :: l0); auto.
-apply (app_ass l2 (a :: nil) l).
-apply (app_ass l2 (a :: nil) l).
-Qed.
-
-(************************************** 
-   A transposition is a permutation
-   **************************************)
- 
-Theorem permutation_transposition :
- forall a b l1 l2 l3,
- permutation (l1 ++ a :: l2 ++ b :: l3) (l1 ++ b :: l2 ++ a :: l3).
-intros a b l1 l2 l3.
-apply permutation_app_comp; auto.
-change
-  (permutation ((a :: nil) ++ l2 ++ (b :: nil) ++ l3)
-     ((b :: nil) ++ l2 ++ (a :: nil) ++ l3)) in |- *.
-repeat rewrite <- app_ass.
-apply permutation_app_comp; auto.
-apply permutation_trans with ((b :: nil) ++ (a :: nil) ++ l2); auto.
-apply permutation_app_swap; auto.
-repeat rewrite app_ass.
-apply permutation_app_comp; auto.
-apply permutation_app_swap; auto.
-Qed.
-
-(************************************** 
-   An element of a list can be put on top of the list to get a permutation
-   **************************************)
- 
-Theorem in_permutation_ex :
- forall a l, In a l -> exists l1 : list A, permutation (a :: l1) l.
-intros a l; elim l; simpl in |- *; auto.
-intros H; case H; auto.
-intros a0 l0 H [H0| H0].
-exists l0; rewrite H0; auto.
-case H; auto; intros l1 Hl1; exists (a0 :: l1).
-apply permutation_trans with (a0 :: a :: l1); auto.
-Qed.
- 
-(************************************** 
-   A permutation of a cons can be inverted
-   **************************************)
-
-Let permutation_cons_ex_aux :
-  forall (a : A) (l1 l2 : list A),
-  permutation l1 l2 ->
-  forall l11 l12 : list A,
-  l1 = l11 ++ a :: l12 ->
-  exists l3 : list A,
-    (exists l4 : list A,
-       l2 = l3 ++ a :: l4 /\ permutation (l11 ++ l12) (l3 ++ l4)).
-intros a l1 l2 H; elim H; clear H l1 l2.
-intros l11 l12; case l11; simpl in |- *; intros; discriminate.
-intros a0 l1 l2 H H0 l11 l12; case l11; simpl in |- *.
-exists (nil (A:=A)); exists l1; simpl in |- *; split; auto.
-injection H1; intros; subst; auto.
-injection H1; intros H2 H3; rewrite <- H2; auto.
-intros a1 l111 H1.
-case (H0 l111 l12); auto.
-injection H1; auto.
-intros l3 (l4, (Hl1, Hl2)).
-exists (a0 :: l3); exists l4; split; simpl in |- *; auto.
-injection H1; intros; subst; auto.
-injection H1; intros H2 H3; rewrite H3; auto.
-intros a0 b l l11 l12; case l11; simpl in |- *.
-case l12; try (intros; discriminate).
-intros a1 l0 H; exists (b :: nil); exists l0; simpl in |- *; split; auto.
-injection H; intros; subst; auto.
-injection H; intros H1 H2 H3; rewrite H2; auto.
-intros a1 l111; case l111; simpl in |- *.
-intros H; exists (nil (A:=A)); exists (a0 :: l12); simpl in |- *; split; auto.
-injection H; intros; subst; auto.
-injection H; intros H1 H2 H3; rewrite H3; auto.
-intros a2 H1111 H; exists (a2 :: a1 :: H1111); exists l12; simpl in |- *;
- split; auto.
-injection H; intros; subst; auto.
-intros l1 l2 l3 H H0 H1 H2 l11 l12 H3.
-case H0 with (1 := H3).
-intros l4 (l5, (Hl1, Hl2)).
-case H2 with (1 := Hl1).
-intros l6 (l7, (Hl3, Hl4)).
-exists l6; exists l7; split; auto.
-apply permutation_trans with (1 := Hl2); auto.
-Qed.
- 
-Theorem permutation_cons_ex :
- forall (a : A) (l1 l2 : list A),
- permutation (a :: l1) l2 ->
- exists l3 : list A,
-   (exists l4 : list A, l2 = l3 ++ a :: l4 /\ permutation l1 (l3 ++ l4)).
-intros a l1 l2 H.
-apply (permutation_cons_ex_aux a (a :: l1) l2 H nil l1); simpl in |- *; auto.
-Qed.
-
-(************************************** 
-   A permutation can be simply inverted if the two list starts with a cons
-   **************************************)
- 
-Theorem permutation_inv :
- forall (a : A) (l1 l2 : list A),
- permutation (a :: l1) (a :: l2) -> permutation l1 l2.
-intros a l1 l2 H; case permutation_cons_ex with (1 := H).
-intros l3 (l4, (Hl1, Hl2)).
-apply permutation_trans with (1 := Hl2).
-generalize Hl1; case l3; simpl in |- *; auto.
-intros H1; injection H1; intros H2; rewrite H2; auto.
-intros a0 l5 H1; injection H1; intros H2 H3; rewrite H2; rewrite H3; auto.
-apply permutation_trans with (a0 :: l4 ++ l5); auto.
-apply permutation_skip; apply permutation_app_swap.
-apply (permutation_app_swap (a0 :: l4) l5).
-Qed.
-
-(************************************** 
-   Take a list and return tle list of all pairs of an element of the 
-   list and the remaining list
-   **************************************)
- 
-Fixpoint split_one (l : list A) : list (A * list A) :=
-  match l with
-  | nil => nil (A:=A * list A)
-  | a :: l1 =>
-      (a, l1)
-      :: map (fun p : A * list A => (fst p, a :: snd p)) (split_one l1)
-  end.
-
-(************************************** 
-   The pairs of the list are a permutation
-   **************************************)
- 
-Theorem split_one_permutation :
- forall (a : A) (l1 l2 : list A),
- In (a, l1) (split_one l2) -> permutation (a :: l1) l2.
-intros a l1 l2; generalize a l1; elim l2; clear a l1 l2; simpl in |- *; auto.
-intros a l1 H1; case H1.
-intros a l H a0 l1 [H0| H0].
-injection H0; intros H1 H2; rewrite H2; rewrite H1; auto.
-generalize H H0; elim (split_one l); simpl in |- *; auto.
-intros H1 H2; case H2.
-intros a1 l0 H1 H2 [H3| H3]; auto.
-injection H3; intros H4 H5; (rewrite <- H4; rewrite <- H5).
-apply permutation_trans with (a :: fst a1 :: snd a1); auto.
-apply permutation_skip.
-apply H2; auto.
-case a1; simpl in |- *; auto.
-Qed.
-
-(************************************** 
-   All elements of the list are there
-   **************************************)
- 
-Theorem split_one_in_ex :
- forall (a : A) (l1 : list A),
- In a l1 -> exists l2 : list A, In (a, l2) (split_one l1).
-intros a l1; elim l1; simpl in |- *; auto.
-intros H; case H.
-intros a0 l H [H0| H0]; auto.
-exists l; left; subst; auto.
-case H; auto.
-intros x H1; exists (a0 :: x); right; auto.
-apply
- (in_map (fun p : A * list A => (fst p, a0 :: snd p)) (split_one l) (a, x));
- auto.
-Qed.
-
-(************************************** 
-   An auxillary function to generate all permutations
-   **************************************)
- 
-Fixpoint all_permutations_aux (l : list A) (n : nat) {struct n} :
- list (list A) :=
-  match n with
-  | O => nil :: nil
-  | S n1 =>
-      flat_map
-        (fun p : A * list A =>
-         map (cons (fst p)) (all_permutations_aux (snd p) n1)) (
-        split_one l)
-  end.
-(************************************** 
-   Generate all the permutations
-   **************************************)
- 
-Definition all_permutations (l : list A) := all_permutations_aux l (length l).
- 
-(************************************** 
-   All the elements of the list are permutations
-   **************************************)
-
-Let all_permutations_aux_permutation :
-  forall (n : nat) (l1 l2 : list A),
-  n = length l2 -> In l1 (all_permutations_aux l2 n) -> permutation l1 l2.
-intros n; elim n; simpl in |- *; auto.
-intros l1 l2; case l2.
-simpl in |- *; intros H0 [H1| H1].
-rewrite <- H1; auto.
-case H1.
-simpl in |- *; intros; discriminate.
-intros n0 H l1 l2 H0 H1.
-case in_flat_map_ex with (1 := H1).
-clear H1; intros x; case x; clear x; intros a1 l3 (H1, H2).
-case in_map_inv with (1 := H2).
-simpl in |- *; intros y (H3, H4).
-rewrite H4; auto.
-apply permutation_trans with (a1 :: l3); auto.
-apply permutation_skip; auto.
-apply H with (2 := H3).
-apply eq_add_S.
-apply trans_equal with (1 := H0).
-change (length l2 = length (a1 :: l3)) in |- *.
-apply permutation_length; auto.
-apply permutation_sym; apply split_one_permutation; auto.
-apply split_one_permutation; auto.
-Qed.
- 
-Theorem all_permutations_permutation :
- forall l1 l2 : list A, In l1 (all_permutations l2) -> permutation l1 l2.
-intros l1 l2 H; apply all_permutations_aux_permutation with (n := length l2);
- auto.
-Qed.
- 
-(************************************** 
-   A permutation is in the list
-   **************************************)
-
-Let permutation_all_permutations_aux :
-  forall (n : nat) (l1 l2 : list A),
-  n = length l2 -> permutation l1 l2 -> In l1 (all_permutations_aux l2 n).
-intros n; elim n; simpl in |- *; auto.
-intros l1 l2; case l2.
-intros H H0; rewrite permutation_nil_inv with (1 := H0); auto with datatypes.
-simpl in |- *; intros; discriminate.
-intros n0 H l1; case l1.
-intros l2 H0 H1;
- rewrite permutation_nil_inv with (1 := permutation_sym _ _ H1) in H0;
- discriminate.
-clear l1; intros a1 l1 l2 H1 H2.
-case (split_one_in_ex a1 l2); auto.
-apply permutation_in with (1 := H2); auto with datatypes.
-intros x H0.
-apply in_flat_map with (b := (a1, x)); auto.
-apply in_map; simpl in |- *.
-apply H; auto.
-apply eq_add_S.
-apply trans_equal with (1 := H1).
-change (length l2 = length (a1 :: x)) in |- *.
-apply permutation_length; auto.
-apply permutation_sym; apply split_one_permutation; auto.
-apply permutation_inv with (a := a1).
-apply permutation_trans with (1 := H2).
-apply permutation_sym; apply split_one_permutation; auto.
-Qed.
- 
-Theorem permutation_all_permutations :
- forall l1 l2 : list A, permutation l1 l2 -> In l1 (all_permutations l2).
-intros l1 l2 H; unfold all_permutations in |- *;
- apply permutation_all_permutations_aux; auto.
-Qed.
-
-(************************************** 
-   Permutation is decidable
-   **************************************)
- 
-Definition permutation_dec :
-  (forall a b : A, {a = b} + {a <> b}) ->
-  forall l1 l2 : list A, {permutation l1 l2} + {~ permutation l1 l2}.
-intros H l1 l2.
-case (In_dec (list_eq_dec H) l1 (all_permutations l2)).
-intros i; left; apply all_permutations_permutation; auto.
-intros i; right; contradict i; apply permutation_all_permutations; auto.
-Defined.
- 
-End permutation.
-
-(************************************** 
-   Hints
-   **************************************)
-
-Hint Constructors permutation.
-Hint Resolve permutation_refl.
-Hint Resolve permutation_app_comp.
-Hint Resolve permutation_app_swap.
-
-(************************************** 
-   Implicits
-   **************************************)
-
-Implicit Arguments permutation [A].
-Implicit Arguments split_one [A].
-Implicit Arguments all_permutations [A].
-Implicit Arguments permutation_dec [A].
-
-(************************************** 
-   Permutation is compatible with map
-   **************************************)
- 
-Theorem permutation_map :
- forall (A B : Set) (f : A -> B) l1 l2,
- permutation l1 l2 -> permutation (map f l1) (map f l2).
-intros A B f l1 l2 H; elim H; simpl in |- *; auto.
-intros l0 l3 l4 H0 H1 H2 H3; apply permutation_trans with (2 := H3); auto.
-Qed.
-Hint Resolve permutation_map.
- 
-(************************************** 
-  Permutation  of a map can be inverted
-  *************************************)
-
-Let permutation_map_ex_aux :
-  forall (A B : Set) (f : A -> B) l1 l2 l3,
-  permutation l1 l2 ->
-  l1 = map f l3 -> exists l4, permutation l4 l3 /\ l2 = map f l4.
-intros A1 B1 f l1 l2 l3 H; generalize l3; elim H; clear H l1 l2 l3.
-intros l3; case l3; simpl in |- *; auto.
-intros H; exists (nil (A:=A1)); auto.
-intros; discriminate.
-intros a0 l1 l2 H H0 l3; case l3; simpl in |- *; auto.
-intros; discriminate.
-intros a1 l H1; case (H0 l); auto.
-injection H1; auto.
-intros l5 (H2, H3); exists (a1 :: l5); split; simpl in |- *; auto.
-injection H1; intros; subst; auto.
-intros a0 b l l3; case l3.
-intros; discriminate.
-intros a1 l0; case l0; simpl in |- *.
-intros; discriminate.
-intros a2 l1 H; exists (a2 :: a1 :: l1); split; simpl in |- *; auto.
-injection H; intros; subst; auto.
-intros l1 l2 l3 H H0 H1 H2 l0 H3.
-case H0 with (1 := H3); auto.
-intros l4 (HH1, HH2).
-case H2 with (1 := HH2); auto.
-intros l5 (HH3, HH4); exists l5; split; auto.
-apply permutation_trans with (1 := HH3); auto.
-Qed.
- 
-Theorem permutation_map_ex :
- forall (A B : Set) (f : A -> B) l1 l2,
- permutation (map f l1) l2 ->
- exists l3, permutation l3 l1 /\ l2 = map f l3.
-intros A0 B f l1 l2 H; apply permutation_map_ex_aux with (l1 := map f l1);
- auto.
-Qed.
-
-(************************************** 
-   Permutation is compatible with flat_map
- **************************************)
- 
-Theorem permutation_flat_map :
- forall (A B : Set) (f : A -> list B) l1 l2,
- permutation l1 l2 -> permutation (flat_map f l1) (flat_map f l2).
-intros A B f l1 l2 H; elim H; simpl in |- *; auto.
-intros a b l; auto.
-repeat rewrite <- app_ass.
-apply permutation_app_comp; auto.
-intros k3 l4 l5 H0 H1 H2 H3; apply permutation_trans with (1 := H1); auto.
-Qed.
diff --git a/coqprime/List/UList.v b/coqprime/List/UList.v
deleted file mode 100644
index 54a0a3da5..000000000
--- a/coqprime/List/UList.v
+++ /dev/null
@@ -1,286 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-(***********************************************************************
-      UList.v                                                                                       
-                                                                                                         
-      Definition of list with distinct elements                                 
-                                                                                                         
-      Definition: ulist                                                                         
-************************************************************************)
-Require Import List.
-Require Import Arith.
-Require Import Permutation.
-Require Import ListSet.
- 
-Section UniqueList.
-Variable A : Set.
-Variable eqA_dec : forall (a b : A),  ({ a = b }) + ({ a <> b }).
-(* A list is unique if there is not twice the same element in the list *)
- 
-Inductive ulist : list A ->  Prop :=
-  ulist_nil: ulist nil
- | ulist_cons: forall a l, ~ In a l -> ulist l ->  ulist (a :: l) .
-Hint Constructors ulist .
-(* Inversion theorem *)
- 
-Theorem ulist_inv: forall a l, ulist (a :: l) ->  ulist l.
-intros a l H; inversion H; auto.
-Qed.
-(* The append of two unique list is unique if the list are distinct *)
- 
-Theorem ulist_app:
- forall l1 l2,
- ulist l1 ->
- ulist l2 -> (forall (a : A), In a l1 -> In a l2 ->  False) ->  ulist (l1 ++ l2).
-intros L1; elim L1; simpl; auto.
-intros a l H l2 H0 H1 H2; apply ulist_cons; simpl; auto.
-red; intros H3; case in_app_or with ( 1 := H3 ); auto; intros H4.
-inversion H0; auto.
-apply H2 with a; auto.
-apply H; auto.
-apply ulist_inv with ( 1 := H0 ); auto.
-intros a0 H3 H4; apply (H2 a0); auto.
-Qed.
-(* Iinversion theorem the appended list *)
- 
-Theorem ulist_app_inv:
- forall l1 l2 (a : A), ulist (l1 ++ l2) -> In a l1 -> In a l2 ->  False.
-intros l1; elim l1; simpl; auto.
-intros a l H l2 a0 H0 [H1|H1] H2.
-inversion H0 as [|a1 l0 H3 H4 H5]; auto.
-case H4; rewrite H1; auto with datatypes.
-apply (H l2 a0); auto.
-apply ulist_inv with ( 1 := H0 ); auto.
-Qed.
-(* Iinversion theorem the appended list *)
- 
-Theorem ulist_app_inv_l: forall (l1 l2 : list A), ulist (l1 ++ l2) ->  ulist l1.
-intros l1; elim l1; simpl; auto.
-intros a l H l2 H0.
-inversion H0 as [|il1 iH1 iH2 il2 [iH4 iH5]]; apply ulist_cons; auto.
-intros H5; case iH2; auto with datatypes.
-apply H with l2; auto.
-Qed.
-(* Iinversion theorem the appended list *)
- 
-Theorem ulist_app_inv_r: forall (l1 l2 : list A), ulist (l1 ++ l2) ->  ulist l2.
-intros l1; elim l1; simpl; auto.
-intros a l H l2 H0; inversion H0; auto.
-Qed.
-(* Uniqueness is decidable *)
- 
-Definition ulist_dec: forall l,  ({ ulist l }) + ({ ~ ulist l }).
-intros l; elim l; auto.
-intros a l1 [H|H]; auto.
-case (In_dec eqA_dec a l1); intros H2; auto.
-right; red; intros H1; inversion H1; auto.
-right; intros H1; case H; apply ulist_inv with ( 1 := H1 ).
-Defined.
-(* Uniqueness is compatible with permutation *)
- 
-Theorem ulist_perm:
- forall (l1 l2 : list A), permutation l1 l2 -> ulist l1 ->  ulist l2.
-intros l1 l2 H; elim H; clear H l1 l2; simpl; auto.
-intros a l1 l2 H0 H1 H2; apply ulist_cons; auto.
-inversion_clear H2 as [|ia il iH1 iH2 [iH3 iH4]]; auto.
-intros H3; case iH1;
- apply permutation_in with ( 1 := permutation_sym _ _ _ H0 ); auto.
-inversion H2; auto.
-intros a b L H0; apply ulist_cons; auto.
-inversion_clear H0 as [|ia il iH1 iH2]; auto.
-inversion_clear iH2 as [|ia il iH3 iH4]; auto.
-intros H; case H; auto.
-intros H1; case iH1; rewrite H1; simpl; auto.
-apply ulist_cons; auto.
-inversion_clear H0 as [|ia il iH1 iH2]; auto.
-intros H; case iH1; simpl; auto.
-inversion_clear H0 as [|ia il iH1 iH2]; auto.
-inversion iH2; auto.
-Qed.
- 
-Theorem ulist_def:
- forall l a,
- In a l -> ulist l ->  ~ (exists l1 , permutation l (a :: (a :: l1)) ).
-intros l a H H0 [l1 H1].
-absurd (ulist (a :: (a :: l1))); auto.
-intros H2; inversion_clear H2; simpl; auto with datatypes.
-apply ulist_perm with ( 1 := H1 ); auto.
-Qed.
- 
-Theorem ulist_incl_permutation:
- forall (l1 l2 : list A),
- ulist l1 -> incl l1 l2 ->  (exists l3 , permutation l2 (l1 ++ l3) ).
-intros l1; elim l1; simpl; auto.
-intros l2 H H0; exists l2; simpl; auto.
-intros a l H l2 H0 H1; auto.
-case (in_permutation_ex _ a l2); auto with datatypes.
-intros l3 Hl3.
-case (H l3); auto.
-apply ulist_inv with ( 1 := H0 ); auto.
-intros b Hb.
-assert (H2: In b (a :: l3)).
-apply permutation_in with ( 1 := permutation_sym _ _ _ Hl3 );
- auto with datatypes.
-simpl in H2 |-; case H2; intros H3; simpl; auto.
-inversion_clear H0 as [|c lc Hk1]; auto.
-case Hk1; subst a; auto.
-intros l4 H4; exists l4.
-apply permutation_trans with (a :: l3); auto.
-apply permutation_sym; auto.
-Qed.
- 
-Theorem ulist_eq_permutation:
- forall (l1 l2 : list A),
- ulist l1 -> incl l1 l2 -> length l1 = length l2 ->  permutation l1 l2.
-intros l1 l2 H1 H2 H3.
-case (ulist_incl_permutation l1 l2); auto.
-intros l3 H4.
-assert (H5: l3 = @nil A).
-generalize (permutation_length _ _ _ H4); rewrite length_app; rewrite H3.
-rewrite plus_comm; case l3; simpl; auto.
-intros a l H5; absurd (lt (length l2) (length l2)); auto with arith.
-pattern (length l2) at 2; rewrite H5; auto with arith.
-replace l1 with (app l1 l3); auto.
-apply permutation_sym; auto.
-rewrite H5; rewrite app_nil_end; auto.
-Qed.
- 
-
-Theorem ulist_incl_length:
- forall (l1 l2 : list A), ulist l1 -> incl l1 l2 ->  le (length l1) (length l2).
-intros l1 l2 H1 Hi; case ulist_incl_permutation with ( 2 := Hi ); auto.
-intros l3 Hl3; rewrite permutation_length with ( 1 := Hl3 ); auto.
-rewrite length_app; simpl; auto with arith.
-Qed.
-
-Theorem ulist_incl2_permutation:
- forall (l1 l2 : list A),
- ulist l1 -> ulist l2 -> incl l1 l2 -> incl l2 l1  ->  permutation l1 l2.
-intros l1 l2 H1 H2 H3 H4.
-apply ulist_eq_permutation; auto.
-apply le_antisym; apply ulist_incl_length; auto.
-Qed.
- 
- 
-Theorem ulist_incl_length_strict:
- forall (l1 l2 : list A),
- ulist l1 -> incl l1 l2 -> ~ incl l2 l1 ->  lt (length l1) (length l2).
-intros l1 l2 H1 Hi Hi0; case ulist_incl_permutation with ( 2 := Hi ); auto.
-intros l3 Hl3; rewrite permutation_length with ( 1 := Hl3 ); auto.
-rewrite length_app; simpl; auto with arith.
-generalize Hl3; case l3; simpl; auto with arith.
-rewrite <- app_nil_end; auto.
-intros H2; case Hi0; auto.
-intros a HH; apply permutation_in with ( 1 := H2 ); auto.
-intros a l Hl0; (rewrite plus_comm; simpl; rewrite plus_comm; auto with arith).
-Qed.
- 
-Theorem in_inv_dec:
- forall (a b : A) l, In a (cons b l) ->  a = b \/ ~ a = b /\ In a l.
-intros a b l H; case (eqA_dec a b); auto; intros H1.
-right; split; auto; inversion H; auto.
-case H1; auto.
-Qed.
- 
-Theorem in_ex_app_first:
- forall (a : A) (l : list A),
- In a l ->
-  (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2) /\ ~ In a l1  ).
-intros a l; elim l; clear l; auto.
-intros H; case H.
-intros a1 l H H1; auto.
-generalize (in_inv_dec _ _ _ H1); intros [H2|[H2 H3]].
-exists (nil (A:=A)); exists l; simpl; split; auto.
-subst; auto.
-case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl;
- split; auto.
-subst; auto.
-intros H4; case H4; auto.
-Qed.
- 
-Theorem ulist_inv_ulist:
- forall (l : list A),
- ~ ulist l ->
-  (exists a ,
-   exists l1 ,
-   exists l2 ,
-   exists l3 , l = l1 ++ ((a :: l2) ++ (a :: l3)) /\ ulist (l1 ++ (a :: l2))    ).
-intros l; elim l  using list_length_ind; clear l.
-intros l; case l; simpl; auto; clear l.
-intros Rec H0; case H0; auto.
-intros a l H H0.
-case (In_dec eqA_dec a l); intros H1; auto.
-case in_ex_app_first with ( 1 := H1 ); intros l1 [l2 [Hl1 Hl2]]; subst l.
-case (ulist_dec l1); intros H2.
-exists a; exists (@nil A); exists l1; exists l2; split; auto.
-simpl; apply ulist_cons; auto.
-case (H l1); auto.
-rewrite length_app; auto with arith.
-intros b [l3 [l4 [l5 [Hl3 Hl4]]]]; subst l1.
-exists b; exists (a :: l3); exists l4; exists (l5 ++ (a :: l2)); split; simpl;
- auto.
-(repeat (rewrite <- ass_app; simpl)); auto.
-apply ulist_cons; auto.
-contradict Hl2; auto.
-replace (l3 ++ (b :: (l4 ++ (b :: l5)))) with ((l3 ++ (b :: l4)) ++ (b :: l5));
- auto with datatypes.
-(repeat (rewrite <- ass_app; simpl)); auto.
-case (H l); auto; intros a1 [l1 [l2 [l3 [Hl3 Hl4]]]]; subst l.
-exists a1; exists (a :: l1); exists l2; exists l3; split; auto.
-simpl; apply ulist_cons; auto.
-contradict H1.
-replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3))))
-     with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)); auto with datatypes.
-(repeat (rewrite <- ass_app; simpl)); auto.
-Qed.
- 
-Theorem incl_length_repetition:
- forall (l1 l2 : list A),
- incl l1 l2 ->
- lt (length l2) (length l1) ->
-  (exists a ,
-   exists ll1 ,
-   exists ll2 ,
-   exists ll3 ,
-   l1 = ll1 ++ ((a :: ll2) ++ (a :: ll3)) /\ ulist (ll1 ++ (a :: ll2))    ).
-intros l1 l2 H H0; apply ulist_inv_ulist.
-intros H1; absurd (le (length l1) (length l2)); auto with arith.
-apply ulist_incl_length; auto.
-Qed.
- 
-End UniqueList.
-Implicit Arguments ulist [A].
-Hint Constructors ulist .
- 
-Theorem ulist_map:
- forall (A B : Set) (f : A ->  B) l,
- (forall x y, (In x l) -> (In y l) ->  f x = f y ->  x = y) -> ulist l ->  ulist (map f l).
-intros a b f l Hf Hl; generalize Hf; elim Hl; clear Hf;  auto.
-simpl; auto.
-intros a1 l1 H1 H2 H3 Hf; simpl.
-apply ulist_cons; auto with datatypes.
-contradict H1.
-case in_map_inv with ( 1 := H1 ); auto with datatypes.
-intros b1 [Hb1 Hb2].
-replace a1 with b1; auto with datatypes.
-Qed.
- 
-Theorem ulist_list_prod:
- forall (A : Set) (l1 l2 : list A),
- ulist l1 -> ulist l2 ->  ulist (list_prod l1 l2).
-intros A l1 l2 Hl1 Hl2; elim Hl1; simpl; auto.
-intros a l H1 H2 H3; apply ulist_app; auto.
-apply ulist_map; auto.
-intros x y _ _ H; inversion H; auto.
-intros p Hp1 Hp2; case H1.
-case in_map_inv with ( 1 := Hp1 ); intros a1 [Ha1 Ha2]; auto.
-case in_list_prod_inv with ( 1 := Hp2 ); intros b1 [c1 [Hb1 [Hb2 Hb3]]]; auto.
-replace a with b1; auto.
-rewrite Ha2 in Hb1; injection Hb1; auto.
-Qed.
diff --git a/coqprime/List/ZProgression.v b/coqprime/List/ZProgression.v
deleted file mode 100644
index 51ce91cdc..000000000
--- a/coqprime/List/ZProgression.v
+++ /dev/null
@@ -1,104 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
-(*************************************************************)
-
-Require Export Iterator.
-Require Import ZArith.
-Require Export UList.
-Open Scope Z_scope.
- 
-Theorem next_n_Z: forall n m,  next_n Zsucc n m = n + Z_of_nat m.
-intros n m; generalize n; elim m; clear n m.
-intros n; simpl; auto with zarith.
-intros m H n.
-replace (n + Z_of_nat (S m)) with (Zsucc n + Z_of_nat m); auto with zarith.
-rewrite <- H; auto with zarith.
-rewrite inj_S; auto with zarith.
-Qed.
- 
-Theorem Zprogression_end:
- forall n m,
-  progression Zsucc n (S m) =
-  app (progression Zsucc n m) (cons (n + Z_of_nat m) nil).
-intros n m; generalize n; elim m; clear n m.
-simpl; intros; apply f_equal2 with ( f := @cons Z ); auto with zarith.
-intros m1 Hm1 n1.
-apply trans_equal with (cons n1 (progression Zsucc (Zsucc n1) (S m1))); auto.
-rewrite Hm1.
-replace (Zsucc n1 + Z_of_nat m1) with (n1 + Z_of_nat (S m1)); auto with zarith.
-replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith.
-rewrite inj_S; auto with zarith.
-Qed.
- 
-Theorem Zprogression_pred_end:
- forall n m,
-  progression Zpred n (S m) =
-  app (progression Zpred n m) (cons (n - Z_of_nat m) nil).
-intros n m; generalize n; elim m; clear n m.
-simpl; intros; apply f_equal2 with ( f := @cons Z ); auto with zarith.
-intros m1 Hm1 n1.
-apply trans_equal with (cons n1 (progression Zpred (Zpred n1) (S m1))); auto.
-rewrite Hm1.
-replace (Zpred n1 - Z_of_nat m1) with (n1 - Z_of_nat (S m1)); auto with zarith.
-replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith.
-rewrite inj_S; auto with zarith.
-Qed.
- 
-Theorem Zprogression_opp:
- forall n m,
-  rev (progression Zsucc n m) = progression Zpred (n + Z_of_nat (pred m)) m.
-intros n m; generalize n; elim m; clear n m.
-simpl; auto.
-intros m Hm n.
-rewrite (Zprogression_end n); auto.
-rewrite distr_rev.
-rewrite Hm; simpl; auto.
-case m.
-simpl; auto.
-intros m1;
- replace (n + Z_of_nat (pred (S m1))) with (Zpred (n + Z_of_nat (S m1))); auto.
-rewrite inj_S; simpl; (unfold Zpred; unfold Zsucc); auto with zarith.
-Qed.
- 
-Theorem Zprogression_le_init:
- forall n m p, In p (progression Zsucc n m) ->  (n <= p).
-intros n m; generalize n; elim m; clear n m; simpl; auto.
-intros; contradiction.
-intros m H n p [H1|H1]; auto with zarith.
-generalize (H _ _ H1); auto with zarith.
-Qed.
- 
-Theorem Zprogression_le_end:
- forall n m p, In p (progression Zsucc n m) ->  (p < n + Z_of_nat m).
-intros n m; generalize n; elim m; clear n m; auto.
-intros; contradiction.
-intros m H n p H1; simpl in H1 |-; case H1; clear H1; intros H1;
- auto with zarith.
-subst n; auto with zarith.
-apply Zle_lt_trans with (p + 0); auto with zarith.
-apply Zplus_lt_compat_l; red; simpl; auto with zarith.
-apply Zlt_le_trans with (Zsucc n + Z_of_nat m); auto with zarith.
-rewrite inj_S; rewrite Zplus_succ_comm; auto with zarith.
-Qed.
- 
-Theorem ulist_Zprogression: forall a n,  ulist (progression Zsucc a n).
-intros a n; generalize a; elim n; clear a n; simpl; auto with zarith.
-intros n H1 a; apply ulist_cons; auto.
-intros H2; absurd (Zsucc a <= a); auto with zarith.
-apply Zprogression_le_init with ( 1 := H2 ).
-Qed.
- 
-Theorem in_Zprogression:
- forall a b n, ( a <= b < a + Z_of_nat n ) ->  In b (progression Zsucc a n).
-intros a b n; generalize a b; elim n; clear a b n; auto with zarith.
-simpl; auto with zarith.
-intros n H a b.
-replace (a + Z_of_nat (S n)) with (Zsucc a + Z_of_nat n); auto with zarith.
-intros [H1 H2]; simpl; auto with zarith.
-case (Zle_lt_or_eq _ _ H1); auto with zarith.
-rewrite inj_S; auto with zarith.
-Qed.