Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of Zdiv

Some details: 

 - ZAux.v is the only file left in Ints/Z. The few elements that remain in it
   are rather specific or compatibility oriented. Others parts and files have 
   been either deleted when unused or pushed into some place of ZArith. 
 - Ints/List/ is removed since it was not needed anymore
 - Ints/Tactic.v disappear: some of its tactic were unused, some already in 
   Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict 
   has been added to Tactics.v
 - Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ...
 - A new file Zpow_facts inherits lots of results about Zpower. Placing them 
   into Zpower would have been difficult with respect to compatibility 
   (import of ring)
 - A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder
 - Adequate adaptations to Ints/num/* (mainly renaming of lemmas) 
 
Now, concerning Zdiv, the behavior when dividing by a negative number is now 
fully proved. When this was possible, existing lemmas has been extended, 
either from strictly positive to non-zero divisor, or even to arbitrary 
divisor (especially when playing with Zmod). These extended lemmas are named
with the suffix _full, whereas the original restrictive lemmas are retained 
for compatibility. Several lemmas now have shorter proofs (based on unicity 
lemmas). Lemmas are now more or less organized by themes (division and order, 
division and usual operations, etc). Three possible choices of spec for 
divisions on negative numbers are presented: this Zdiv, the ocaml approach
and the remainder-always-positive approach. The ugly behavior of Zopp 
with the current choice of Zdiv/Zmod is now fully covered. A embryo of 
division "a la Ocaml" is given: Odiv and Omod. 




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10291 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 0 insertions, 1352 deletions

diff --git a/theories/Ints/List/Iterator.v b/theories/Ints/List/Iterator.v
deleted file mode 100644
index 327a1454b6..0000000000
--- a/theories/Ints/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 LPermutation.
-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/theories/Ints/List/LPermutation.v b/theories/Ints/List/LPermutation.v
deleted file mode 100644
index 9270ded432..0000000000
--- a/theories/Ints/List/LPermutation.v
+++ /dev/null
@@ -1,509 +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.
-eq_tac.
-injection H2; auto.
-apply permutation_nil_inv; auto.
-injection H2; intros H3 H4; rewrite <- H3; auto.
-apply permutation_sym; 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.
-eq_tac; injection H1; 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.
-eq_tac; injection H1; 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.
-repeat eq_tac; injection H; 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.
-repeat eq_tac; injection H; auto.
-injection H; intros H1 H2 H3; rewrite H3; auto.
-intros a2 H1111 H; exists (a2 :: a1 :: H1111); exists l12; simpl in |- *;
- split; auto.
-repeat eq_tac; injection H; 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; eq_tac; 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.
-eq_tac; auto; injection H1; 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.
-repeat eq_tac; injection H; 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/theories/Ints/List/ListAux.v b/theories/Ints/List/ListAux.v
deleted file mode 100644
index 5a6541c957..0000000000
--- a/theories/Ints/List/ListAux.v
+++ /dev/null
@@ -1,272 +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.
-eq_tac; auto.
-case H; auto; intros l1 [l2 Hl2]; exists (a1 :: l1); exists l2; simpl; auto.
-eq_tac; 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; eq_tac; auto.
-apply H with ( 1 := 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; eq_tac; injection H0; auto.
-intros b l0 H0; case (H l2 l0 l4 a0); auto.
-injection H0; auto.
-intros [l5 H1].
-left; exists l5; eq_tac; injection H0; 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.
-eq_tac; auto.
-intros b0 l0 H0; left; exists l0; injection H0; intros; (repeat eq_tac); auto.
-intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto.
-injection H0; auto.
-intros [l5 HH1]; left; exists l5; eq_tac; auto; injection H0; auto.
-intros [H1|[H1 H2]]; auto.
-right; right; split; auto; eq_tac; auto; injection H0; 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)).
-eq_tac; 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; eq_tac; 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.
-eq_tac; 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/theories/Ints/List/UList.v b/theories/Ints/List/UList.v
deleted file mode 100644
index 5248a8b1f8..0000000000
--- a/theories/Ints/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.
-eq_tac; auto.
-case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl;
- split; auto.
-eq_tac; 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/theories/Ints/List/ZProgression.v b/theories/Ints/List/ZProgression.v
deleted file mode 100644
index e4c15e38db..0000000000
--- a/theories/Ints/List/ZProgression.v
+++ /dev/null
@@ -1,105 +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.
-unfold Zpred; ring.
-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.