Import coqprime; use it to prove Euler's criterion.

5 files changed, 1347 insertions, 0 deletions

diff --git a/coqprime/List/Iterator.v b/coqprime/List/Iterator.v
new file mode 100644
index 000000000..96d3e5655
--- /dev/null
+++ b/coqprime/List/Iterator.v
@@ -0,0 +1,180 @@
+
+(*************************************************************)
+(*      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
new file mode 100644
index 000000000..c3c9602bd
--- /dev/null
+++ b/coqprime/List/ListAux.v
@@ -0,0 +1,271 @@
+
+(*************************************************************)
+(*      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
new file mode 100644
index 000000000..a06693f89
--- /dev/null
+++ b/coqprime/List/Permutation.v
@@ -0,0 +1,506 @@
+
+(*************************************************************)
+(*      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
new file mode 100644
index 000000000..54a0a3da5
--- /dev/null
+++ b/coqprime/List/UList.v
@@ -0,0 +1,286 @@
+
+(*************************************************************)
+(*      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
new file mode 100644
index 000000000..51ce91cdc
--- /dev/null
+++ b/coqprime/List/ZProgression.v
@@ -0,0 +1,104 @@
+
+(*************************************************************)
+(*      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.