From 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 Mon Sep 17 00:00:00 2001
From: notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 17 Oct 2006 12:53:34 +0000
Subject: Mise en forme des theories

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Sets/Classical_sets.v           | 187 +++++-----
 theories/Sets/Constructive_sets.v        | 229 ++++++------
 theories/Sets/Cpo.v                      | 103 +++---
 theories/Sets/Ensembles.v                | 101 +++---
 theories/Sets/Finite_sets.v              |  64 ++--
 theories/Sets/Finite_sets_facts.v        | 581 +++++++++++++++----------------
 theories/Sets/Image.v                    | 320 ++++++++---------
 theories/Sets/Infinite_sets.v            | 386 ++++++++++----------
 theories/Sets/Integers.v                 | 221 ++++++------
 theories/Sets/Multiset.v                 | 304 ++++++++--------
 theories/Sets/Partial_Order.v            | 114 +++---
 theories/Sets/Permut.v                   | 142 ++++----
 theories/Sets/Powerset_Classical_facts.v | 576 +++++++++++++++---------------
 theories/Sets/Powerset_facts.v           | 434 +++++++++++------------
 14 files changed, 1860 insertions(+), 1902 deletions(-)

(limited to 'theories/Sets')

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index a21534bd5..62fd4df1a 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -30,103 +30,98 @@ Require Export Ensembles.
 Require Export Constructive_sets.
 Require Export Classical_Type.
 
-(* Hints Unfold  not . *)
-
 Section Ensembles_classical.
-Variable U : Type.
-
-Lemma not_included_empty_Inhabited :
- forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
-Proof.
-intros A NI.
-elim (not_all_ex_not U (fun x:U => ~ In U A x)).
-intros x H; apply Inhabited_intro with x.
-apply NNPP; auto with sets.
-red in |- *; intro.
-apply NI; red in |- *.
-intros x H'; elim (H x); trivial with sets.
-Qed.
-Hint Resolve not_included_empty_Inhabited.
-
-Lemma not_empty_Inhabited :
- forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
-Proof.
-intros; apply not_included_empty_Inhabited.
-red in |- *; auto with sets.
-Qed.
-
-Lemma Inhabited_Setminus :
- forall X Y:Ensemble U,
-   Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
-Proof.
-intros X Y I NI. 
-elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
-intros x YX.
-apply Inhabited_intro with x.
-apply Setminus_intro.
-apply not_imply_elim with (In U X x); trivial with sets.
-auto with sets.
-Qed.
-Hint Resolve Inhabited_Setminus.
-
-Lemma Strict_super_set_contains_new_element :
- forall X Y:Ensemble U,
-   Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
-Proof.
-auto 7 with sets.
-Qed.
-Hint Resolve Strict_super_set_contains_new_element.
-
-Lemma Subtract_intro :
- forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
-Proof.
-unfold Subtract at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Subtract_intro.
-
-Lemma Subtract_inv :
- forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
-Proof.
-intros A x y H'; elim H'; auto with sets.
-Qed.
-
-Lemma Included_Strict_Included :
- forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
-Proof.
-intros X Y H'; try assumption.
-elim (classic (X = Y)); auto with sets.
-Qed.
-
-Lemma Strict_Included_inv :
- forall X Y:Ensemble U,
-   Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
-Proof.
-intros X Y H'; red in H'.
-split; [ tauto | idtac ].
-elim H'; intros H'0 H'1; try exact H'1; clear H'.
-apply Strict_super_set_contains_new_element; auto with sets.
-Qed.
-
-Lemma not_SIncl_empty :
- forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
-Proof.
-intro X; red in |- *; intro H'; try exact H'.
-lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
-intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
-intros x H'0; elim H'0.
-intro H'3; elim H'3.
-Qed.
-
-Lemma Complement_Complement :
- forall A:Ensemble U, Complement U (Complement U A) = A.
-Proof.
-unfold Complement in |- *; intros; apply Extensionality_Ensembles;
- auto with sets.
-red in |- *; split; auto with sets.
-red in |- *; intros; apply NNPP; auto with sets.
-Qed.
+  Variable U : Type.
+
+  Lemma not_included_empty_Inhabited :
+    forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
+  Proof.
+    intros A NI.
+    elim (not_all_ex_not U (fun x:U => ~ In U A x)).
+    intros x H; apply Inhabited_intro with x.
+    apply NNPP; auto with sets.
+    red in |- *; intro.
+    apply NI; red in |- *.
+    intros x H'; elim (H x); trivial with sets.
+  Qed.
+
+  Lemma not_empty_Inhabited :
+    forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
+  Proof.
+    intros; apply not_included_empty_Inhabited.
+    red in |- *; auto with sets.
+  Qed.
+
+  Lemma Inhabited_Setminus :
+    forall X Y:Ensemble U,
+      Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
+  Proof.
+    intros X Y I NI. 
+    elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
+    intros x YX.
+    apply Inhabited_intro with x.
+    apply Setminus_intro.
+    apply not_imply_elim with (In U X x); trivial with sets.
+    auto with sets.
+  Qed.
+
+  Lemma Strict_super_set_contains_new_element :
+    forall X Y:Ensemble U,
+      Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
+  Proof.
+    auto 7 using Inhabited_Setminus with sets.
+  Qed.
+
+  Lemma Subtract_intro :
+    forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
+  Proof.
+    unfold Subtract at 1 in |- *; auto with sets.
+  Qed.
+  Hint Resolve Subtract_intro : sets.
+  
+  Lemma Subtract_inv :
+    forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
+  Proof.
+    intros A x y H'; elim H'; auto with sets.
+  Qed.
+
+  Lemma Included_Strict_Included :
+    forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
+  Proof.
+    intros X Y H'; try assumption.
+    elim (classic (X = Y)); auto with sets.
+  Qed.
+
+  Lemma Strict_Included_inv :
+    forall X Y:Ensemble U,
+      Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
+  Proof.
+    intros X Y H'; red in H'.
+    split; [ tauto | idtac ].
+    elim H'; intros H'0 H'1; try exact H'1; clear H'.
+    apply Strict_super_set_contains_new_element; auto with sets.
+  Qed.
+
+  Lemma not_SIncl_empty :
+    forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
+  Proof.
+    intro X; red in |- *; intro H'; try exact H'.
+    lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
+    intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
+    intros x H'0; elim H'0.
+    intro H'3; elim H'3.
+  Qed.
+
+  Lemma Complement_Complement :
+    forall A:Ensemble U, Complement U (Complement U A) = A.
+  Proof.
+    unfold Complement in |- *; intros; apply Extensionality_Ensembles;
+      auto with sets.
+    red in |- *; split; auto with sets.
+    red in |- *; intros; apply NNPP; auto with sets.
+  Qed.
 
 End Ensembles_classical.
 
-Hint Resolve Strict_super_set_contains_new_element Subtract_intro
-  not_SIncl_empty: sets v62.
\ No newline at end of file
+ Hint Resolve Strict_super_set_contains_new_element Subtract_intro
+  not_SIncl_empty: sets v62.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 09a941bcd..65ce03e28 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -29,131 +29,118 @@
 Require Export Ensembles.
 
 Section Ensembles_facts.
-Variable U : Type.
-
-Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
-Proof.
-intros B C H'; rewrite H'; auto with sets.
-Qed.
-
-Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
-Proof.
-red in |- *; destruct 1.
-Qed.
-Hint Resolve Noone_in_empty.
-
-Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
-Proof.
-intro; red in |- *.
-intros x H; elim (Noone_in_empty x); auto with sets.
-Qed.
-Hint Resolve Included_Empty.
-
-Lemma Add_intro1 :
- forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
-Proof.
-unfold Add at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Add_intro1.
-
-Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
-Proof.
-unfold Add at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Add_intro2.
-
-Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
-Proof.
-intros A x.
-apply Inhabited_intro with (x := x); auto with sets.
-Qed.
-Hint Resolve Inhabited_add.
-
-Lemma Inhabited_not_empty :
- forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
-Proof.
-intros X H'; elim H'.
-intros x H'0; red in |- *; intro H'1.
-absurd (In U X x); auto with sets.
-rewrite H'1; auto with sets.
-Qed.
-Hint Resolve Inhabited_not_empty.
-
-Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.
-Proof.
-auto with sets.
-Qed.
-Hint Resolve Add_not_Empty.
-
-Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
-Proof.
-intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
-Qed.
-Hint Resolve not_Empty_Add.
-
-Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
-Proof.
-intros x y H'; elim H'; trivial with sets.
-Qed.
-Hint Resolve Singleton_inv.
-
-Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.
-Proof.
-intros x y H'; rewrite H'; trivial with sets.
-Qed.
-Hint Resolve Singleton_intro.
-
-Lemma Union_inv :
- forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.
-Proof.
-intros B C x H'; elim H'; auto with sets.
-Qed.
-
-Lemma Add_inv :
- forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
-Proof.
-intros A x y H'; elim H'; auto with sets.
-Qed.
-
-Lemma Intersection_inv :
- forall (B C:Ensemble U) (x:U),
-   In U (Intersection U B C) x -> In U B x /\ In U C x.
-Proof.
-intros B C x H'; elim H'; auto with sets.
-Qed.
-Hint Resolve Intersection_inv.
-
-Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.
-Proof.
-intros x y z H'; elim H'; auto with sets.
-Qed.
-Hint Resolve Couple_inv.
-
-Lemma Setminus_intro :
- forall (A B:Ensemble U) (x:U),
-   In U A x -> ~ In U B x -> In U (Setminus U A B) x.
-Proof.
-unfold Setminus at 1 in |- *; red in |- *; auto with sets.
-Qed.
-Hint Resolve Setminus_intro.
+  Variable U : Type.
+  
+  Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
+  Proof.
+    intros B C H'; rewrite H'; auto with sets.
+  Qed.
+
+  Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
+  Proof.
+    red in |- *; destruct 1.
+  Qed.
+
+  Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
+  Proof.
+    intro; red in |- *.
+    intros x H; elim (Noone_in_empty x); auto with sets.
+  Qed.
+
+  Lemma Add_intro1 :
+    forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
+  Proof.
+    unfold Add at 1 in |- *; auto with sets.
+  Qed.
+  
+  Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
+  Proof.
+    unfold Add at 1 in |- *; auto with sets.
+  Qed.
+
+  Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
+  Proof.
+    intros A x.
+    apply Inhabited_intro with (x := x); auto using Add_intro2 with sets.
+  Qed.
+
+  Lemma Inhabited_not_empty :
+    forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
+  Proof.
+    intros X H'; elim H'.
+    intros x H'0; red in |- *; intro H'1.
+    absurd (In U X x); auto with sets.
+    rewrite H'1; auto using Noone_in_empty with sets.
+  Qed.
+
+  Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.
+  Proof.
+    intros A x; apply Inhabited_not_empty; apply Inhabited_add.
+  Qed.
+
+  Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
+  Proof.
+    intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
+  Qed.
+
+  Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
+  Proof.
+    intros x y H'; elim H'; trivial with sets.
+  Qed.
+
+  Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.
+  Proof.
+    intros x y H'; rewrite H'; trivial with sets.
+  Qed.
+
+  Lemma Union_inv :
+    forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.
+  Proof.
+    intros B C x H'; elim H'; auto with sets.
+  Qed.
+  
+  Lemma Add_inv :
+    forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
+  Proof.
+    intros A x y H'; induction H'. 
+      left; assumption.
+      right; apply Singleton_inv; assumption.
+  Qed.
+  
+  Lemma Intersection_inv :
+    forall (B C:Ensemble U) (x:U),
+      In U (Intersection U B C) x -> In U B x /\ In U C x.
+  Proof.
+    intros B C x H'; elim H'; auto with sets.
+  Qed.
+
+  Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.
+  Proof.
+    intros x y z H'; elim H'; auto with sets.
+  Qed.
+
+  Lemma Setminus_intro :
+    forall (A B:Ensemble U) (x:U),
+      In U A x -> ~ In U B x -> In U (Setminus U A B) x.
+  Proof.
+    unfold Setminus at 1 in |- *; red in |- *; auto with sets.
+  Qed.
  
-Lemma Strict_Included_intro :
- forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
-Proof.
-auto with sets.
-Qed.
-Hint Resolve Strict_Included_intro.
-
-Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
-Proof.
-intro X; red in |- *; intro H'; elim H'.
-intros H'0 H'1; elim H'1; auto with sets.
-Qed.
-Hint Resolve Strict_Included_strict.
+  Lemma Strict_Included_intro :
+    forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
+  Proof.
+    auto with sets.
+  Qed.
+
+  Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
+  Proof.
+    intro X; red in |- *; intro H'; elim H'.
+    intros H'0 H'1; elim H'1; auto with sets.
+  Qed.
 
 End Ensembles_facts.
 
 Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
   Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
   Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
-  not_Empty_Add Inhabited_add Included_Empty: sets v62.
\ No newline at end of file
+  not_Empty_Add Inhabited_add Included_Empty: sets v62.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index efd83c106..c1e64babc 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -31,79 +31,80 @@ Require Export Relations_1.
 Require Export Partial_Order.
 
 Section Bounds.
-Variable U : Type.
-Variable D : PO U.
+  Variable U : Type.
+  Variable D : PO U.
 
-Let C := Carrier_of U D.
+  Let C := Carrier_of U D.
+  
+  Let R := Rel_of U D.
 
-Let R := Rel_of U D.
-
-Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
+  Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
     Upper_Bound_definition :
-      In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
+    In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
 
-Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
+  Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
     Lower_Bound_definition :
-      In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
-
-Inductive Lub (B:Ensemble U) (x:U) : Prop :=
+    In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
+  
+  Inductive Lub (B:Ensemble U) (x:U) : Prop :=
     Lub_definition :
-      Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
+    Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
 
-Inductive Glb (B:Ensemble U) (x:U) : Prop :=
+  Inductive Glb (B:Ensemble U) (x:U) : Prop :=
     Glb_definition :
-      Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
+    Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
 
-Inductive Bottom (bot:U) : Prop :=
+  Inductive Bottom (bot:U) : Prop :=
     Bottom_definition :
-      In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
-
-Inductive Totally_ordered (B:Ensemble U) : Prop :=
+    In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
+  
+  Inductive Totally_ordered (B:Ensemble U) : Prop :=
     Totally_ordered_definition :
-      (Included U B C ->
-       forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
-      Totally_ordered B.
+    (Included U B C ->
+      forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
+    Totally_ordered B.
 
-Definition Compatible : Relation U :=
-  fun x y:U =>
-    In U C x ->
-    In U C y ->  exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
-	
-Inductive Directed (X:Ensemble U) : Prop :=
-    Definition_of_Directed :
-      Included U X C ->
-      Inhabited U X ->
-      (forall x1 x2:U,
-         Included U (Couple U x1 x2) X ->
-          exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
-      Directed X.
+  Definition Compatible : Relation U :=
+    fun x y:U =>
+      In U C x ->
+      In U C y ->  exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
 
-Inductive Complete : Prop :=
+  Inductive Directed (X:Ensemble U) : Prop :=
+    Definition_of_Directed :
+    Included U X C ->
+    Inhabited U X ->
+    (forall x1 x2:U,
+      Included U (Couple U x1 x2) X ->
+      exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
+    Directed X.
+  
+  Inductive Complete : Prop :=
     Definition_of_Complete :
-      (exists bot : _, Bottom bot) ->
-      (forall X:Ensemble U, Directed X ->  exists bsup : _, Lub X bsup) ->
-      Complete.
+    (exists bot : _, Bottom bot) ->
+    (forall X:Ensemble U, Directed X ->  exists bsup : _, Lub X bsup) ->
+    Complete.
 
-Inductive Conditionally_complete : Prop :=
+  Inductive Conditionally_complete : Prop :=
     Definition_of_Conditionally_complete :
-      (forall X:Ensemble U,
-         Included U X C ->
-         (exists maj : _, Upper_Bound X maj) ->
-          exists bsup : _, Lub X bsup) -> Conditionally_complete.
+    (forall X:Ensemble U,
+      Included U X C ->
+      (exists maj : _, Upper_Bound X maj) ->
+      exists bsup : _, Lub X bsup) -> Conditionally_complete.
 End Bounds.
+
 Hint Resolve Totally_ordered_definition Upper_Bound_definition
   Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
   Definition_of_Complete Definition_of_Complete
   Definition_of_Conditionally_complete.
 
 Section Specific_orders.
-Variable U : Type.
-
-Record Cpo : Type := Definition_of_cpo
-  {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
-
-Record Chain : Type := Definition_of_chain
-  {PO_of_chain : PO U;
-   Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
+  Variable U : Type.
+
+  Record Cpo : Type := Definition_of_cpo
+    {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
+  
+  Record Chain : Type := Definition_of_chain
+    {PO_of_chain : PO U;
+    Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
 
 End Specific_orders.
\ No newline at end of file
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 9c85d67d0..339298572 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -27,69 +27,68 @@
 (*i $Id$ i*)
 
 Section Ensembles.
-Variable U : Type.
-
-Definition Ensemble := U -> Prop. 
-
-Definition In (A:Ensemble) (x:U) : Prop := A x.
-
-Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
-
-Inductive Empty_set : Ensemble :=.
-
-Inductive Full_set : Ensemble :=
+  Variable U : Type.
+  
+  Definition Ensemble := U -> Prop. 
+
+  Definition In (A:Ensemble) (x:U) : Prop := A x.
+  
+  Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
+  
+  Inductive Empty_set : Ensemble :=.
+  
+  Inductive Full_set : Ensemble :=
     Full_intro : forall x:U, In Full_set x.
 
 (** NB: The following definition builds-in equality of elements in [U] as 
-   Leibniz equality. 
+     Leibniz equality. 
 
-   This may have to be changed if we replace [U] by a Setoid on [U] 
-   with its own equality [eqs], with  
-   [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
+     This may have to be changed if we replace [U] by a Setoid on [U] 
+     with its own equality [eqs], with  
+     [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
 
-Inductive Singleton (x:U) : Ensemble :=
+  Inductive Singleton (x:U) : Ensemble :=
     In_singleton : In (Singleton x) x.
 
-Inductive Union (B C:Ensemble) : Ensemble :=
-  | Union_introl : forall x:U, In B x -> In (Union B C) x
-  | Union_intror : forall x:U, In C x -> In (Union B C) x.
-
-Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
+  Inductive Union (B C:Ensemble) : Ensemble :=
+    | Union_introl : forall x:U, In B x -> In (Union B C) x
+    | Union_intror : forall x:U, In C x -> In (Union B C) x.
 
-Inductive Intersection (B C:Ensemble) : Ensemble :=
+  Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
+  
+  Inductive Intersection (B C:Ensemble) : Ensemble :=
     Intersection_intro :
-      forall x:U, In B x -> In C x -> In (Intersection B C) x.
-
-Inductive Couple (x y:U) : Ensemble :=
-  | Couple_l : In (Couple x y) x
-  | Couple_r : In (Couple x y) y.
-
-Inductive Triple (x y z:U) : Ensemble :=
-  | Triple_l : In (Triple x y z) x
-  | Triple_m : In (Triple x y z) y
-  | Triple_r : In (Triple x y z) z.
-
-Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
-
-Definition Setminus (B C:Ensemble) : Ensemble :=
-  fun x:U => In B x /\ ~ In C x.
-
-Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
-
-Inductive Disjoint (B C:Ensemble) : Prop :=
+    forall x:U, In B x -> In C x -> In (Intersection B C) x.
+
+  Inductive Couple (x y:U) : Ensemble :=
+    | Couple_l : In (Couple x y) x
+    | Couple_r : In (Couple x y) y.
+  
+  Inductive Triple (x y z:U) : Ensemble :=
+    | Triple_l : In (Triple x y z) x
+    | Triple_m : In (Triple x y z) y
+    | Triple_r : In (Triple x y z) z.
+  
+  Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
+  
+  Definition Setminus (B C:Ensemble) : Ensemble :=
+    fun x:U => In B x /\ ~ In C x.
+  
+  Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
+  
+  Inductive Disjoint (B C:Ensemble) : Prop :=
     Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C.
 
-Inductive Inhabited (B:Ensemble) : Prop :=
+  Inductive Inhabited (B:Ensemble) : Prop :=
     Inhabited_intro : forall x:U, In B x -> Inhabited B.
+  
+  Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
+  
+  Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
+  
+  (** Extensionality Axiom *)
 
-Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
-
-Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
-
-(** Extensionality Axiom *)
-
-Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.
-Hint Resolve Extensionality_Ensembles.
+  Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.
 
 End Ensembles.
 
@@ -98,4 +97,4 @@ Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets
 
 Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
   Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
-  Extensionality_Ensembles: sets v62.
\ No newline at end of file
+  Extensionality_Ensembles: sets v62.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 53981ea8d..a75c3b767 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -29,17 +29,17 @@
 Require Import Ensembles.
 
 Section Ensembles_finis.
-Variable U : Type.
+  Variable U : Type.
 
-Inductive Finite : Ensemble U -> Prop :=
-  | Empty_is_finite : Finite (Empty_set U)
-  | Union_is_finite :
+  Inductive Finite : Ensemble U -> Prop :=
+    | Empty_is_finite : Finite (Empty_set U)
+    | Union_is_finite :
       forall A:Ensemble U,
         Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).
 
-Inductive cardinal : Ensemble U -> nat -> Prop :=
-  | card_empty : cardinal (Empty_set U) 0
-  | card_add :
+  Inductive cardinal : Ensemble U -> nat -> Prop :=
+    | card_empty : cardinal (Empty_set U) 0
+    | card_add :
       forall (A:Ensemble U) (n:nat),
         cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n).
 
@@ -51,31 +51,31 @@ Hint Resolve card_empty card_add: sets v62.
 Require Import Constructive_sets.
 
 Section Ensembles_finis_facts.
-Variable U : Type.
+  Variable U : Type.
+  
+  Lemma cardinal_invert :
+    forall (X:Ensemble U) (p:nat),
+      cardinal U X p ->
+      match p with
+	| O => X = Empty_set U
+	| S n =>
+          exists A : _,
+            (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
+      end.
+  Proof.
+    induction 1; simpl in |- *; auto.
+    exists A; exists x; auto.
+  Qed.
 
-Lemma cardinal_invert :
- forall (X:Ensemble U) (p:nat),
-   cardinal U X p ->
-   match p with
-   | O => X = Empty_set U
-   | S n =>
-        exists A : _,
-         (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
-   end.
-Proof.
-induction 1; simpl in |- *; auto.
-exists A; exists x; auto.
-Qed.
-
-Lemma cardinal_elim :
- forall (X:Ensemble U) (p:nat),
-   cardinal U X p ->
-   match p with
-   | O => X = Empty_set U
-   | S n => Inhabited U X
-   end.
-Proof.
-intros X p C; elim C; simpl in |- *; trivial with sets.
-Qed.
+  Lemma cardinal_elim :
+    forall (X:Ensemble U) (p:nat),
+      cardinal U X p ->
+      match p with
+	| O => X = Empty_set U
+	| S n => Inhabited U X
+      end.
+  Proof.
+    intros X p C; elim C; simpl in |- *; trivial with sets.
+  Qed.
 
 End Ensembles_finis_facts.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 94ea964c2..0615c9c9d 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -37,311 +37,308 @@ Require Export Gt.
 Require Export Lt.
 
 Section Finite_sets_facts.
-Variable U : Type.
+  Variable U : Type.
 
-Lemma finite_cardinal :
- forall X:Ensemble U, Finite U X ->  exists n : nat, cardinal U X n.
-Proof.
-induction 1 as [| A _ [n H]].
-exists 0; auto with sets.
-exists (S n); auto with sets.
-Qed.
+  Lemma finite_cardinal :
+    forall X:Ensemble U, Finite U X ->  exists n : nat, cardinal U X n.
+  Proof.
+    induction 1 as [| A _ [n H]].
+    exists 0; auto with sets.
+    exists (S n); auto with sets.
+  Qed.
 
-Lemma cardinal_finite :
- forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
-Proof.
-induction 1; auto with sets.
-Qed.
+  Lemma cardinal_finite :
+    forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
+  Proof.
+    induction 1; auto with sets.
+  Qed.
 
-Theorem Add_preserves_Finite :
- forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
-Proof.
-intros X x H'.
-elim (classic (In U X x)); intro H'0; auto with sets.
-rewrite (Non_disjoint_union U X x); auto with sets.
-Qed.
-Hint Resolve Add_preserves_Finite.
+  Theorem Add_preserves_Finite :
+    forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
+  Proof.
+    intros X x H'.
+    elim (classic (In U X x)); intro H'0; auto with sets.
+    rewrite (Non_disjoint_union U X x); auto with sets.
+  Qed.
 
-Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
-Proof.
-intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
-change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
-Qed.
-Hint Resolve Singleton_is_finite.
+  Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
+  Proof.
+    intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
+    change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
+  Qed.
 
-Theorem Union_preserves_Finite :
- forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
-Proof.
-intros X Y H'; elim H'.
-rewrite (Empty_set_zero U Y); auto with sets.
-intros A H'0 H'1 x H'2 H'3.
-rewrite (Union_commutative U (Add U A x) Y).
-rewrite <- (Union_add U Y A x).
-rewrite (Union_commutative U Y A); auto with sets.
-Qed.
+  Theorem Union_preserves_Finite :
+    forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
+  Proof.
+    intros X Y H; induction H as [|A Fin_A Hind x].
+    rewrite (Empty_set_zero U Y). trivial.
+    intros. 
+    rewrite (Union_commutative U (Add U A x) Y).
+    rewrite <- (Union_add U Y A x).
+    rewrite (Union_commutative U Y A).
+    apply Add_preserves_Finite.
+    apply Hind. assumption.
+  Qed.
 
-Lemma Finite_downward_closed :
- forall A:Ensemble U,
-   Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
-Proof.
-intros A H'; elim H'; auto with sets.
-intros X H'0.
-rewrite (less_than_empty U X H'0); auto with sets.
-intros; elim Included_Add with U X A0 x; auto with sets.
-destruct 1 as [A' [H5 H6]].
-rewrite H5; auto with sets.
-Qed.
+  Lemma Finite_downward_closed :
+    forall A:Ensemble U,
+      Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
+  Proof.
+    intros A H'; elim H'; auto with sets.
+    intros X H'0.
+    rewrite (less_than_empty U X H'0); auto with sets.
+    intros; elim Included_Add with U X A0 x; auto with sets.
+    destruct 1 as [A' [H5 H6]].
+    rewrite H5; auto with sets.
+  Qed.
 
-Lemma Intersection_preserves_finite :
- forall A:Ensemble U,
-   Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
-Proof.
-intros A H' X; apply Finite_downward_closed with A; auto with sets.
-Qed.
+  Lemma Intersection_preserves_finite :
+    forall A:Ensemble U,
+      Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
+  Proof.
+    intros A H' X; apply Finite_downward_closed with A; auto with sets.
+  Qed.
+  
+  Lemma cardinalO_empty :
+    forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
+  Proof.
+    intros X H; apply (cardinal_invert U X 0); trivial with sets.
+  Qed.
 
-Lemma cardinalO_empty :
- forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
-Proof.
-intros X H; apply (cardinal_invert U X 0); trivial with sets.
-Qed.
-Hint Resolve cardinalO_empty.
+  Lemma inh_card_gt_O :
+    forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
+  Proof.
+    induction 1 as [x H'].
+    intros n H'0.
+    elim (gt_O_eq n); auto with sets.
+    intro H'1; generalize H'; generalize H'0.
+    rewrite <- H'1; intro H'2.
+    rewrite (cardinalO_empty X); auto with sets.
+    intro H'3; elim H'3.
+  Qed.
 
-Lemma inh_card_gt_O :
- forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
-Proof.
-induction 1 as [x H'].
-intros n H'0.
-elim (gt_O_eq n); auto with sets.
-intro H'1; generalize H'; generalize H'0.
-rewrite <- H'1; intro H'2.
-rewrite (cardinalO_empty X); auto with sets.
-intro H'3; elim H'3.
-Qed.
+  Lemma card_soustr_1 :
+    forall (X:Ensemble U) (n:nat),
+      cardinal U X n ->
+      forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
+  Proof.
+    intros X n H'; elim H'.
+    intros x H'0; elim H'0.
+    clear H' n X.
+    intros X n H' H'0 x H'1 x0 H'2.
+    elim (classic (In U X x0)).
+    intro H'4; rewrite (add_soustr_xy U X x x0).
+    elim (classic (x = x0)).
+    intro H'5.
+    absurd (In U X x0); auto with sets.
+    rewrite <- H'5; auto with sets.
+    intro H'3; try assumption.
+    cut (S (pred n) = pred (S n)).
+    intro H'5; rewrite <- H'5.
+    apply card_add; auto with sets.
+    red in |- *; intro H'6; elim H'6.
+    intros H'7 H'8; try assumption.
+    elim H'1; auto with sets.
+    unfold pred at 2 in |- *; symmetry  in |- *.
+    apply S_pred with (m := 0).
+    change (n > 0) in |- *.
+    apply inh_card_gt_O with (X := X); auto with sets.
+    apply Inhabited_intro with (x := x0); auto with sets.
+    red in |- *; intro H'3.
+    apply H'1.
+    elim H'3; auto with sets.
+    rewrite H'3; auto with sets.
+    elim (classic (x = x0)).
+    intro H'3; rewrite <- H'3.
+    cut (Subtract U (Add U X x) x = X); auto with sets.
+    intro H'4; rewrite H'4; auto with sets.
+    intros H'3 H'4; try assumption.
+    absurd (In U (Add U X x) x0); auto with sets.
+    red in |- *; intro H'5; try exact H'5.
+    lapply (Add_inv U X x x0); tauto.
+  Qed.
 
-Lemma card_soustr_1 :
- forall (X:Ensemble U) (n:nat),
-   cardinal U X n ->
-   forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
-Proof.
-intros X n H'; elim H'.
-intros x H'0; elim H'0.
-clear H' n X.
-intros X n H' H'0 x H'1 x0 H'2.
-elim (classic (In U X x0)).
-intro H'4; rewrite (add_soustr_xy U X x x0).
-elim (classic (x = x0)).
-intro H'5.
-absurd (In U X x0); auto with sets.
-rewrite <- H'5; auto with sets.
-intro H'3; try assumption.
-cut (S (pred n) = pred (S n)).
-intro H'5; rewrite <- H'5.
-apply card_add; auto with sets.
-red in |- *; intro H'6; elim H'6.
-intros H'7 H'8; try assumption.
-elim H'1; auto with sets.
-unfold pred at 2 in |- *; symmetry  in |- *.
-apply S_pred with (m := 0).
-change (n > 0) in |- *.
-apply inh_card_gt_O with (X := X); auto with sets.
-apply Inhabited_intro with (x := x0); auto with sets.
-red in |- *; intro H'3.
-apply H'1.
-elim H'3; auto with sets.
-rewrite H'3; auto with sets.
-elim (classic (x = x0)).
-intro H'3; rewrite <- H'3.
-cut (Subtract U (Add U X x) x = X); auto with sets.
-intro H'4; rewrite H'4; auto with sets.
-intros H'3 H'4; try assumption.
-absurd (In U (Add U X x) x0); auto with sets.
-red in |- *; intro H'5; try exact H'5.
-lapply (Add_inv U X x x0); tauto.
-Qed.
+  Lemma cardinal_is_functional :
+    forall (X:Ensemble U) (c1:nat),
+      cardinal U X c1 ->
+      forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
+  Proof.
+    intros X c1 H'; elim H'.
+    intros Y c2 H'0; elim H'0; auto with sets.
+    intros A n H'1 H'2 x H'3 H'5.
+    elim (not_Empty_Add U A x); auto with sets.
+    clear H' c1 X.
+    intros X n H' H'0 x H'1 Y c2 H'2.
+    elim H'2.
+    intro H'3.
+    elim (not_Empty_Add U X x); auto with sets.
+    clear H'2 c2 Y.
+    intros X0 c2 H'2 H'3 x0 H'4 H'5.
+    elim (classic (In U X0 x)).
+    intro H'6; apply f_equal with nat.
+    apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+    elimtype (pred (S c2) = c2); auto with sets.
+    apply card_soustr_1; auto with sets.
+    rewrite <- H'5.
+    apply Sub_Add_new; auto with sets.
+    elim (classic (x = x0)).
+    intros H'6 H'7; apply f_equal with nat.
+    apply H'0 with (Y := X0); auto with sets.
+    apply Simplify_add with (x := x); auto with sets.
+    pattern x at 2 in |- *; rewrite H'6; auto with sets.
+    intros H'6 H'7.
+    absurd (Add U X x = Add U X0 x0); auto with sets.
+    clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
+    red in |- *; intro H'.
+    lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
+    clear H'.
+    intro H'; red in H'.
+    elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
+    absurd (In U (Add U X0 x0) x); auto with sets.
+    lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
+  Qed.
 
-Lemma cardinal_is_functional :
- forall (X:Ensemble U) (c1:nat),
-   cardinal U X c1 ->
-   forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
-Proof.
-intros X c1 H'; elim H'.
-intros Y c2 H'0; elim H'0; auto with sets.
-intros A n H'1 H'2 x H'3 H'5.
-elim (not_Empty_Add U A x); auto with sets.
-clear H' c1 X.
-intros X n H' H'0 x H'1 Y c2 H'2.
-elim H'2.
-intro H'3.
-elim (not_Empty_Add U X x); auto with sets.
-clear H'2 c2 Y.
-intros X0 c2 H'2 H'3 x0 H'4 H'5.
-elim (classic (In U X0 x)).
-intro H'6; apply f_equal with nat.
-apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-elimtype (pred (S c2) = c2); auto with sets.
-apply card_soustr_1; auto with sets.
-rewrite <- H'5.
-apply Sub_Add_new; auto with sets.
-elim (classic (x = x0)).
-intros H'6 H'7; apply f_equal with nat.
-apply H'0 with (Y := X0); auto with sets.
-apply Simplify_add with (x := x); auto with sets.
-pattern x at 2 in |- *; rewrite H'6; auto with sets.
-intros H'6 H'7.
-absurd (Add U X x = Add U X0 x0); auto with sets.
-clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
-red in |- *; intro H'.
-lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
-clear H'.
-intro H'; red in H'.
-elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
-absurd (In U (Add U X0 x0) x); auto with sets.
-lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
-Qed.
+  Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
+  Proof.
+    intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
+    elim m; auto with sets.
+    intros; elim H0; intros; elim H1; intros; elim H2; intros.
+    elim (not_Empty_Add U x x0 H3).
+  Qed.
 
-Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
-Proof.
-intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
-elim m; auto with sets.
-intros; elim H0; intros; elim H1; intros; elim H2; intros.
-elim (not_Empty_Add U x x0 H3).
-Qed.
+  Lemma cardinal_unicity :
+    forall (X:Ensemble U) (n:nat),
+      cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
+  Proof.
+    intros; apply cardinal_is_functional with X X; auto with sets.
+  Qed.
+  
+  Lemma card_Add_gen :
+    forall (A:Ensemble U) (x:U) (n n':nat),
+      cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
+  Proof.
+    intros A x n n' H'.
+    elim (classic (In U A x)).
+    intro H'0.
+    rewrite (Non_disjoint_union U A x H'0).
+    intro H'1; cut (n = n').
+    intro E; rewrite E; auto with sets.
+    apply cardinal_unicity with A; auto with sets.
+    intros H'0 H'1.
+    cut (n' = S n).
+    intro E; rewrite E; auto with sets.
+    apply cardinal_unicity with (Add U A x); auto with sets.
+  Qed.
 
-Lemma cardinal_unicity :
- forall (X:Ensemble U) (n:nat),
-   cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
-Proof.
-intros; apply cardinal_is_functional with X X; auto with sets.
-Qed.
+  Lemma incl_st_card_lt :
+    forall (X:Ensemble U) (c1:nat),
+      cardinal U X c1 ->
+      forall (Y:Ensemble U) (c2:nat),
+	cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
+  Proof.
+    intros X c1 H'; elim H'.
+    intros Y c2 H'0; elim H'0; auto with sets arith.
+    intro H'1.
+    elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
+    clear H' c1 X.
+    intros X n H' H'0 x H'1 Y c2 H'2.
+    elim H'2.
+    intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
+    clear H'2 c2 Y.
+    intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
+    intro H'6; apply gt_n_S.
+    apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+    elimtype (pred (S c2) = c2); auto with sets arith.
+    apply card_soustr_1; auto with sets arith.
+    apply incl_st_add_soustr; auto with sets arith.
+    elim (classic (x = x0)).
+    intros H'6 H'7; apply gt_n_S.
+    apply H'0 with (Y := X0); auto with sets arith.
+    apply sincl_add_x with (x := x0).
+    rewrite <- H'6; auto with sets arith.
+    pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
+    intros H'6 H'7; red in H'5.
+    elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
+    red in H'8.
+    generalize (H'8 x).
+    intro H'5; lapply H'5; auto with sets arith.
+    intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
+    intro; absurd (In U X0 x); auto with sets arith.
+    intro; absurd (x = x0); auto with sets arith.
+  Qed.
 
-Lemma card_Add_gen :
- forall (A:Ensemble U) (x:U) (n n':nat),
-   cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
-Proof.
-intros A x n n' H'.
-elim (classic (In U A x)).
-intro H'0.
-rewrite (Non_disjoint_union U A x H'0).
-intro H'1; cut (n = n').
-intro E; rewrite E; auto with sets.
-apply cardinal_unicity with A; auto with sets.
-intros H'0 H'1.
-cut (n' = S n).
-intro E; rewrite E; auto with sets.
-apply cardinal_unicity with (Add U A x); auto with sets.
-Qed.
+  Lemma incl_card_le :
+    forall (X Y:Ensemble U) (n m:nat),
+      cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
+  Proof.
+    intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
+    cut (m > n); auto with sets arith.
+    apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
+    generalize H0; rewrite <- H2; intro.
+    cut (n = m).
+    intro E; rewrite E; auto with sets arith.
+    apply cardinal_unicity with X; auto with sets arith.
+  Qed.
+  
+  Lemma G_aux :
+    forall P:Ensemble U -> Prop,
+      (forall X:Ensemble U,
+	Finite U X ->
+	(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+      P (Empty_set U).
+  Proof.
+    intros P H'; try assumption.
+    apply H'; auto with sets.
+    clear H'; auto with sets.
+    intros Y H'; try assumption.
+    red in H'.
+    elim H'; intros H'0 H'1; try exact H'1; clear H'.
+    lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
+    elim H'1; auto with sets.
+  Qed.
 
-Lemma incl_st_card_lt :
- forall (X:Ensemble U) (c1:nat),
-   cardinal U X c1 ->
-   forall (Y:Ensemble U) (c2:nat),
-     cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
-Proof.
-intros X c1 H'; elim H'.
-intros Y c2 H'0; elim H'0; auto with sets arith.
-intro H'1.
-elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
-clear H' c1 X.
-intros X n H' H'0 x H'1 Y c2 H'2.
-elim H'2.
-intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
-clear H'2 c2 Y.
-intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
-intro H'6; apply gt_n_S.
-apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-elimtype (pred (S c2) = c2); auto with sets arith.
-apply card_soustr_1; auto with sets arith.
-apply incl_st_add_soustr; auto with sets arith.
-elim (classic (x = x0)).
-intros H'6 H'7; apply gt_n_S.
-apply H'0 with (Y := X0); auto with sets arith.
-apply sincl_add_x with (x := x0).
-rewrite <- H'6; auto with sets arith.
-pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
-intros H'6 H'7; red in H'5.
-elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
-red in H'8.
-generalize (H'8 x).
-intro H'5; lapply H'5; auto with sets arith.
-intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
-intro; absurd (In U X0 x); auto with sets arith.
-intro; absurd (x = x0); auto with sets arith.
-Qed.
+  Lemma Generalized_induction_on_finite_sets :
+    forall P:Ensemble U -> Prop,
+      (forall X:Ensemble U,
+	Finite U X ->
+	(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+      forall X:Ensemble U, Finite U X -> P X.
+  Proof.
+    intros P H'0 X H'1.
+    generalize P H'0; clear H'0 P.
+    elim H'1.
+    intros P H'0.
+    apply G_aux; auto with sets.
+    clear H'1 X.
+    intros A H' H'0 x H'1 P H'3.
+    cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
+    generalize H'1.
+    apply H'0.
+    intros X K H'5 L Y H'6; apply H'3; auto with sets.
+    apply Finite_downward_closed with (A := Add U X x); auto with sets.
+    intros Y0 H'7.
+    elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
+      auto with sets.
+    intros H'2 H'4.
+    elim (Included_Add U Y0 X x);
+      [ intro H'14
+	| intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
+	| idtac ]; auto with sets.
+    elim (Included_Strict_Included U Y0 X); auto with sets.
+    intro H'9; apply H'5 with (Y := Y0); auto with sets.
+    intro H'9; rewrite H'9.
+    apply H'3; auto with sets.
+    intros Y1 H'8; elim H'8.
+    intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
+    elim (Included_Strict_Included U A' X); auto with sets.
+    intro H'8; apply H'5 with (Y := A'); auto with sets.
+    rewrite <- H'15; auto with sets.
+    intro H'8.
+    elim H'7.
+    intros H'9 H'10; apply H'10 || elim H'10; try assumption.
+    generalize H'6.
+    rewrite <- H'8.
+    rewrite <- H'15; auto with sets.
+  Qed.
 
-Lemma incl_card_le :
- forall (X Y:Ensemble U) (n m:nat),
-   cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
-Proof.
-intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
-cut (m > n); auto with sets arith.
-apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
-generalize H0; rewrite <- H2; intro.
-cut (n = m).
-intro E; rewrite E; auto with sets arith.
-apply cardinal_unicity with X; auto with sets arith.
-Qed.
-
-Lemma G_aux :
- forall P:Ensemble U -> Prop,
-   (forall X:Ensemble U,
-      Finite U X ->
-      (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
-   P (Empty_set U).
-Proof.
-intros P H'; try assumption.
-apply H'; auto with sets.
-clear H'; auto with sets.
-intros Y H'; try assumption.
-red in H'.
-elim H'; intros H'0 H'1; try exact H'1; clear H'.
-lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
-elim H'1; auto with sets.
-Qed.
-
-Hint Unfold not.
-
-Lemma Generalized_induction_on_finite_sets :
- forall P:Ensemble U -> Prop,
-   (forall X:Ensemble U,
-      Finite U X ->
-      (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
-   forall X:Ensemble U, Finite U X -> P X.
-Proof.
-intros P H'0 X H'1.
-generalize P H'0; clear H'0 P.
-elim H'1.
-intros P H'0.
-apply G_aux; auto with sets.
-clear H'1 X.
-intros A H' H'0 x H'1 P H'3.
-cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
-generalize H'1.
-apply H'0.
-intros X K H'5 L Y H'6; apply H'3; auto with sets.
-apply Finite_downward_closed with (A := Add U X x); auto with sets.
-intros Y0 H'7.
-elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
- auto with sets.
-intros H'2 H'4.
-elim (Included_Add U Y0 X x);
- [ intro H'14
- | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
- | idtac ]; auto with sets.
-elim (Included_Strict_Included U Y0 X); auto with sets.
-intro H'9; apply H'5 with (Y := Y0); auto with sets.
-intro H'9; rewrite H'9.
-apply H'3; auto with sets.
-intros Y1 H'8; elim H'8.
-intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
-elim (Included_Strict_Included U A' X); auto with sets.
-intro H'8; apply H'5 with (Y := A'); auto with sets.
-rewrite <- H'15; auto with sets.
-intro H'8.
-elim H'7.
-intros H'9 H'10; apply H'10 || elim H'10; try assumption.
-generalize H'6.
-rewrite <- H'8.
-rewrite <- H'15; auto with sets.
-Qed.
-
-End Finite_sets_facts.
\ No newline at end of file
+End Finite_sets_facts.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 469b41783..da3aec320 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -39,167 +39,167 @@ Require Export Le.
 Require Export Finite_sets_facts.
 
 Section Image.
-Variables U V : Type.
-
-Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
+  Variables U V : Type.
+  
+  Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
     Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y.
+  
+  Lemma Im_def :
+    forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
+  Proof.
+    intros X f x H'; try assumption.
+    apply Im_intro with (x := x); auto with sets.
+  Qed.
+
+  Lemma Im_add :
+    forall (X:Ensemble U) (x:U) (f:U -> V),
+      Im (Add _ X x) f = Add _ (Im X f) (f x).
+  Proof.
+    intros X x f.
+    apply Extensionality_Ensembles.
+    split; red in |- *; intros x0 H'.
+    elim H'; intros.
+    rewrite H0.
+    elim Add_inv with U X x x1; auto using Im_def with sets.
+    destruct 1; auto using Im_def with sets.
+    elim Add_inv with V (Im X f) (f x) x0. 
+    destruct 1 as [x0 H y H0].
+    rewrite H0; auto using Im_def with sets.
+    destruct 1; auto using Im_def with sets.
+    trivial.
+  Qed.
+  
+  Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
+  Proof.
+    intro f; try assumption.
+    apply Extensionality_Ensembles.
+    split; auto with sets.
+    red in |- *.
+    intros x H'; elim H'.
+    intros x0 H'0; elim H'0; auto with sets.
+  Qed.
+
+  Lemma finite_image :
+    forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
+  Proof.
+    intros X f H'; elim H'.
+    rewrite (image_empty f); auto with sets.
+    intros A H'0 H'1 x H'2; clear H' X.
+    rewrite (Im_add A x f); auto with sets.
+    apply Add_preserves_Finite; auto with sets.
+  Qed.
+  
+  Lemma Im_inv :
+    forall (X:Ensemble U) (f:U -> V) (y:V),
+      In _ (Im X f) y ->  exists x : U, In _ X x /\ f x = y.
+  Proof.
+    intros X f y H'; elim H'.
+    intros x H'0 y0 H'1; rewrite H'1.
+    exists x; auto with sets.
+  Qed.
+  
+  Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
+  
+  Lemma not_injective_elim :
+    forall f:U -> V,
+      ~ injective f ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
+  Proof.
+    unfold injective in |- *; intros f H.
+    cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
+    2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
+      trivial with sets.
+    destruct 1 as [x C]; exists x.
+    cut (exists y : _, ~ (f x = f y -> x = y)).
+    2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
+      trivial with sets.
+    destruct 1 as [y D]; exists y.
+    apply imply_to_and; trivial with sets.
+  Qed.
+  
+  Lemma cardinal_Im_intro :
+    forall (A:Ensemble U) (f:U -> V) (n:nat),
+      cardinal _ A n ->  exists p : nat, cardinal _ (Im A f) p.
+  Proof.
+    intros.
+    apply finite_cardinal; apply finite_image.
+    apply cardinal_finite with n; trivial with sets.
+  Qed.
+  
+  Lemma In_Image_elim :
+    forall (A:Ensemble U) (f:U -> V),
+      injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
+  Proof.
+    intros.
+    elim Im_inv with A f (f x); trivial with sets.
+    intros z C; elim C; intros InAz E.
+    elim (H z x E); trivial with sets.
+  Qed.
+  
+  Lemma injective_preserves_cardinal :
+    forall (A:Ensemble U) (f:U -> V) (n:nat),
+      injective f ->
+      cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
+  Proof.
+    induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.
+    rewrite (image_empty f).
+    intros n' CE.
+    apply cardinal_unicity with V (Empty_set V); auto with sets.
+    intro n'.
+    rewrite (Im_add A x f).
+    intro H'3.
+    elim cardinal_Im_intro with A f n; trivial with sets.
+    intros i CI.
+    lapply (H'1 i); trivial with sets.
+    cut (~ In _ (Im A f) (f x)).
+    intros H0 H1.
+    apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
+    apply card_add; auto with sets.
+    rewrite <- H1; trivial with sets.
+    red in |- *; intro; apply H'2.
+    apply In_Image_elim with f; trivial with sets.
+  Qed.
+  
+  Lemma cardinal_decreases :
+    forall (A:Ensemble U) (f:U -> V) (n:nat),
+      cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
+  Proof.
+    induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.
+    rewrite (image_empty f); intros.
+    cut (n' = 0).
+    intro E; rewrite E; trivial with sets.
+    apply cardinal_unicity with V (Empty_set V); auto with sets.
+    intro n'.
+    rewrite (Im_add A x f).
+    elim cardinal_Im_intro with A f n; trivial with sets.
+    intros p C H'3.
+    apply le_trans with (S p).
+    apply card_Add_gen with V (Im A f) (f x); trivial with sets.
+    apply le_n_S; auto with sets.
+  Qed.
+
+  Theorem Pigeonhole :
+    forall (A:Ensemble U) (f:U -> V) (n:nat),
+      cardinal U A n ->
+      forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
+  Proof.
+    unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
+    cut (n' = n).
+    intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
+    apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
+      trivial with sets.
+  Qed.
+  
+  Lemma Pigeonhole_principle :
+    forall (A:Ensemble U) (f:U -> V) (n:nat),
+      cardinal _ A n ->
+      forall n':nat,
+	cardinal _ (Im A f) n' ->
+	n' < n ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
+  Proof.
+    intros; apply not_injective_elim.
+    apply Pigeonhole with A n n'; trivial with sets.
+  Qed.
 
-Lemma Im_def :
- forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
-Proof.
-intros X f x H'; try assumption.
-apply Im_intro with (x := x); auto with sets.
-Qed.
-Hint Resolve Im_def.
-
-Lemma Im_add :
- forall (X:Ensemble U) (x:U) (f:U -> V),
-   Im (Add _ X x) f = Add _ (Im X f) (f x).
-Proof.
-intros X x f.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x0 H'.
-elim H'; intros.
-rewrite H0.
-elim Add_inv with U X x x1; auto with sets.
-destruct 1; auto with sets.
-elim Add_inv with V (Im X f) (f x) x0; auto with sets.
-destruct 1 as [x0 H y H0].
-rewrite H0; auto with sets.
-destruct 1; auto with sets.
-Qed.
-
-Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
-Proof.
-intro f; try assumption.
-apply Extensionality_Ensembles.
-split; auto with sets.
-red in |- *.
-intros x H'; elim H'.
-intros x0 H'0; elim H'0; auto with sets.
-Qed.
-Hint Resolve image_empty.
-
-Lemma finite_image :
- forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
-Proof.
-intros X f H'; elim H'.
-rewrite (image_empty f); auto with sets.
-intros A H'0 H'1 x H'2; clear H' X.
-rewrite (Im_add A x f); auto with sets.
-apply Add_preserves_Finite; auto with sets.
-Qed.
-Hint Resolve finite_image.
-
-Lemma Im_inv :
- forall (X:Ensemble U) (f:U -> V) (y:V),
-   In _ (Im X f) y ->  exists x : U, In _ X x /\ f x = y.
-Proof.
-intros X f y H'; elim H'.
-intros x H'0 y0 H'1; rewrite H'1.
-exists x; auto with sets.
-Qed.
-
-Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
-
-Lemma not_injective_elim :
- forall f:U -> V,
-   ~ injective f ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
-Proof.
-unfold injective in |- *; intros f H.
-cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
-2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
-    trivial with sets.
-destruct 1 as [x C]; exists x.
-cut (exists y : _, ~ (f x = f y -> x = y)).
-2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
-    trivial with sets.
-destruct 1 as [y D]; exists y.
-apply imply_to_and; trivial with sets.
-Qed.
-
-Lemma cardinal_Im_intro :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
-   cardinal _ A n ->  exists p : nat, cardinal _ (Im A f) p.
-Proof.
-intros.
-apply finite_cardinal; apply finite_image.
-apply cardinal_finite with n; trivial with sets.
-Qed.
-
-Lemma In_Image_elim :
- forall (A:Ensemble U) (f:U -> V),
-   injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
-Proof.
-intros.
-elim Im_inv with A f (f x); trivial with sets.
-intros z C; elim C; intros InAz E.
-elim (H z x E); trivial with sets.
-Qed.
-
-Lemma injective_preserves_cardinal :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
-   injective f ->
-   cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
-Proof.
-induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.
-rewrite (image_empty f).
-intros n' CE.
-apply cardinal_unicity with V (Empty_set V); auto with sets.
-intro n'.
-rewrite (Im_add A x f).
-intro H'3.
-elim cardinal_Im_intro with A f n; trivial with sets.
-intros i CI.
-lapply (H'1 i); trivial with sets.
-cut (~ In _ (Im A f) (f x)).
-intros H0 H1.
-apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
-apply card_add; auto with sets.
-rewrite <- H1; trivial with sets.
-red in |- *; intro; apply H'2.
-apply In_Image_elim with f; trivial with sets.
-Qed.
-
-Lemma cardinal_decreases :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
-   cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
-Proof.
-induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.
-rewrite (image_empty f); intros.
-cut (n' = 0).
-intro E; rewrite E; trivial with sets.
-apply cardinal_unicity with V (Empty_set V); auto with sets.
-intro n'.
-rewrite (Im_add A x f).
-elim cardinal_Im_intro with A f n; trivial with sets.
-intros p C H'3.
-apply le_trans with (S p).
-apply card_Add_gen with V (Im A f) (f x); trivial with sets.
-apply le_n_S; auto with sets.
-Qed.
-
-Theorem Pigeonhole :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
-   cardinal U A n ->
-   forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
-Proof.
-unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
-cut (n' = n).
-intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
-apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
- trivial with sets.
-Qed.
-
-Lemma Pigeonhole_principle :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
-   cardinal _ A n ->
-   forall n':nat,
-     cardinal _ (Im A f) n' ->
-     n' < n ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
-Proof.
-intros; apply not_injective_elim.
-apply Pigeonhole with A n n'; trivial with sets.
-Qed.
 End Image.
+
 Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index c3492ba78..f30c5b763 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -40,205 +40,205 @@ Require Export Finite_sets_facts.
 Require Export Image.
 
 Section Approx.
-Variable U : Type.
+  Variable U : Type.
 
-Inductive Approximant (A X:Ensemble U) : Prop :=
+  Inductive Approximant (A X:Ensemble U) : Prop :=
     Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
 End Approx.
 
 Hint Resolve Defn_of_Approximant.
 
 Section Infinite_sets.
-Variable U : Type.
-
-Lemma make_new_approximant :
- forall A X:Ensemble U,
-   ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
-Proof.
-intros A X H' H'0.
-elim H'0; intros H'1 H'2.
-apply Strict_super_set_contains_new_element; auto with sets.
-red in |- *; intro H'3; apply H'.
-rewrite <- H'3; auto with sets.
-Qed.
-
-Lemma approximants_grow :
- forall A X:Ensemble U,
-   ~ Finite U A ->
-   forall n:nat,
-     cardinal U X n ->
-     Included U X A ->  exists Y : _, cardinal U Y (S n) /\ Included U Y A.
-Proof.
-intros A X H' n H'0; elim H'0; auto with sets.
-intro H'1.
-cut (Inhabited U (Setminus U A (Empty_set U))).
-intro H'2; elim H'2.
-intros x H'3.
-exists (Add U (Empty_set U) x); auto with sets.
-split.
-apply card_add; auto with sets.
-cut (In U A x).
-intro H'4; red in |- *; auto with sets.
-intros x0 H'5; elim H'5; auto with sets.
-intros x1 H'6; elim H'6; auto with sets.
-elim H'3; auto with sets.
-apply make_new_approximant; auto with sets.
-intros A0 n0 H'1 H'2 x H'3 H'5.
-lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
-intros x0 H'2; try assumption.
-elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
-elim (make_new_approximant A x0); auto with sets.
-intros x1 H'2; try assumption.
-exists (Add U x0 x1); auto with sets.
-split.
-apply card_add; auto with sets.
-elim H'2; auto with sets.
-red in |- *.
-intros x2 H'9; elim H'9; auto with sets.
-intros x3 H'10; elim H'10; auto with sets.
-elim H'2; auto with sets.
-auto with sets.
-apply Defn_of_Approximant; auto with sets.
-apply cardinal_finite with (n := S n0); auto with sets.
-Qed.
-
-Lemma approximants_grow' :
- forall A X:Ensemble U,
-   ~ Finite U A ->
-   forall n:nat,
-     cardinal U X n ->
-     Approximant U A X ->
-      exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
-Proof.
-intros A X H' n H'0 H'1; try assumption.
-elim H'1.
-intros H'2 H'3.
-elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).
-intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
-exists x; auto with sets.
-split; [ auto with sets | idtac ].
-apply Defn_of_Approximant; auto with sets.
-apply cardinal_finite with (n := S n); auto with sets.
-apply approximants_grow with (X := X); auto with sets.
-Qed.
-
-Lemma approximant_can_be_any_size :
- forall A X:Ensemble U,
-   ~ Finite U A ->
-   forall n:nat,  exists Y : _, cardinal U Y n /\ Approximant U A Y.
-Proof.
-intros A H' H'0 n; elim n.
-exists (Empty_set U); auto with sets.
-intros n0 H'1; elim H'1.
-intros x H'2.
-apply approximants_grow' with (X := x); tauto.
-Qed.
-
-Variable V : Type.
-
-Theorem Image_set_continuous :
- forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
-   Finite V X ->
-   Included V X (Im U V A f) ->
-    exists n : _,
-     (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
-Proof.
-intros A f X H'; elim H'.
-intro H'0; exists 0.
-exists (Empty_set U); auto with sets.
-intros A0 H'0 H'1 x H'2 H'3; try assumption.
-lapply H'1;
- [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
- auto with sets.
-intros x0 H'1; try assumption.
-exists (S n); try assumption.
-elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
- clear H'4 H'1.
-clear E.
-generalize H'2.
-rewrite <- H'5.
-intro H'1; try assumption.
-red in H'3.
-generalize (H'3 x).
-intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
- auto with sets.
-specialize  5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
- intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
- auto with sets.
-intros x1 H'4; try assumption.
-apply ex_intro with (x := Add U x0 x1).
-split; [ split; [ try assumption | idtac ] | idtac ].
-apply card_add; auto with sets.
-red in |- *; intro H'9; try exact H'9.
-apply H'1.
-elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
-elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
-red in |- *; auto with sets.
-intros x2 H'4; elim H'4; auto with sets.
-intros x3 H'11; elim H'11; auto with sets.
-elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
-apply Im_add; auto with sets.
-Qed.
-
-Theorem Image_set_continuous' :
- forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
-   Approximant V (Im U V A f) X ->
-    exists Y : _, Approximant U A Y /\ Im U V Y f = X.
-Proof.
-intros A f X H'; try assumption.
-cut
- (exists n : _,
-    (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
-intro H'0; elim H'0; intros n E; elim E; clear H'0.
-intros x H'0; try assumption.
-elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
- clear H'1 H'0; auto with sets.
-exists x.
-split; [ idtac | try assumption ].
-apply Defn_of_Approximant; auto with sets.
-apply cardinal_finite with (n := n); auto with sets.
-apply Image_set_continuous; auto with sets.
-elim H'; auto with sets.
-elim H'; auto with sets.
-Qed.
-
-Theorem Pigeonhole_bis :
- forall (A:Ensemble U) (f:U -> V),
-   ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
-Proof.
-intros A f H'0 H'1; try assumption.
-elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
-intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
-elim (make_new_approximant A x); auto with sets.
-intros x0 H'2; elim H'2.
-intros H'5 H'6.
-elim (finite_cardinal V (Im U V A f)); auto with sets.
-intros n E.
-elim (finite_cardinal U x); auto with sets.
-intros n0 E0.
-apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
-apply card_add; auto with sets.
-rewrite (Im_add U V x x0 f); auto with sets.
-cut (In V (Im U V x f) (f x0)).
-intro H'8.
-rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
-rewrite H'4; auto with sets.
-elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
-apply le_lt_n_Sm.
-apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
- auto with sets.
-rewrite H'4; auto with sets.
-elim H'3; auto with sets.
-Qed.
-
-Theorem Pigeonhole_ter :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
-   injective U V f -> Finite V (Im U V A f) -> Finite U A.
-Proof.
-intros A f H' H'0 H'1.
-apply NNPP.
-red in |- *; intro H'2.
-elim (Pigeonhole_bis A f); auto with sets.
-Qed.
+  Variable U : Type.
+  
+  Lemma make_new_approximant :
+    forall A X:Ensemble U,
+      ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
+  Proof.
+    intros A X H' H'0.
+    elim H'0; intros H'1 H'2.
+    apply Strict_super_set_contains_new_element; auto with sets.
+    red in |- *; intro H'3; apply H'.
+    rewrite <- H'3; auto with sets.
+  Qed.
+  
+  Lemma approximants_grow :
+    forall A X:Ensemble U,
+      ~ Finite U A ->
+      forall n:nat,
+	cardinal U X n ->
+	Included U X A ->  exists Y : _, cardinal U Y (S n) /\ Included U Y A.
+  Proof.
+    intros A X H' n H'0; elim H'0; auto with sets.
+    intro H'1.
+    cut (Inhabited U (Setminus U A (Empty_set U))).
+    intro H'2; elim H'2.
+    intros x H'3.
+    exists (Add U (Empty_set U) x); auto with sets.
+    split.
+    apply card_add; auto with sets.
+    cut (In U A x).
+    intro H'4; red in |- *; auto with sets.
+    intros x0 H'5; elim H'5; auto with sets.
+    intros x1 H'6; elim H'6; auto with sets.
+    elim H'3; auto with sets.
+    apply make_new_approximant; auto with sets.
+    intros A0 n0 H'1 H'2 x H'3 H'5.
+    lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
+    intros x0 H'2; try assumption.
+    elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
+    elim (make_new_approximant A x0); auto with sets.
+    intros x1 H'2; try assumption.
+    exists (Add U x0 x1); auto with sets.
+    split.
+    apply card_add; auto with sets.
+    elim H'2; auto with sets.
+    red in |- *.
+    intros x2 H'9; elim H'9; auto with sets.
+    intros x3 H'10; elim H'10; auto with sets.
+    elim H'2; auto with sets.
+    auto with sets.
+    apply Defn_of_Approximant; auto with sets.
+    apply cardinal_finite with (n := S n0); auto with sets.
+  Qed.
+  
+  Lemma approximants_grow' :
+    forall A X:Ensemble U,
+      ~ Finite U A ->
+      forall n:nat,
+	cardinal U X n ->
+	Approximant U A X ->
+	exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
+  Proof.
+    intros A X H' n H'0 H'1; try assumption.
+    elim H'1.
+    intros H'2 H'3.
+    elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).
+    intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
+    exists x; auto with sets.
+    split; [ auto with sets | idtac ].
+    apply Defn_of_Approximant; auto with sets.
+    apply cardinal_finite with (n := S n); auto with sets.
+    apply approximants_grow with (X := X); auto with sets.
+  Qed.
+  
+  Lemma approximant_can_be_any_size :
+    forall A X:Ensemble U,
+      ~ Finite U A ->
+      forall n:nat,  exists Y : _, cardinal U Y n /\ Approximant U A Y.
+  Proof.
+    intros A H' H'0 n; elim n.
+    exists (Empty_set U); auto with sets.
+    intros n0 H'1; elim H'1.
+    intros x H'2.
+    apply approximants_grow' with (X := x); tauto.
+  Qed.
+
+  Variable V : Type.
+  
+  Theorem Image_set_continuous :
+    forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+      Finite V X ->
+      Included V X (Im U V A f) ->
+      exists n : _,
+	(exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
+  Proof.
+    intros A f X H'; elim H'.
+    intro H'0; exists 0.
+    exists (Empty_set U); auto with sets.
+    intros A0 H'0 H'1 x H'2 H'3; try assumption.
+    lapply H'1;
+      [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
+      auto with sets.
+    intros x0 H'1; try assumption.
+    exists (S n); try assumption.
+    elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
+      clear H'4 H'1.
+    clear E.
+    generalize H'2.
+    rewrite <- H'5.
+    intro H'1; try assumption.
+    red in H'3.
+    generalize (H'3 x).
+    intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
+      auto with sets.
+    specialize  5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+      intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
+	auto with sets.
+    intros x1 H'4; try assumption.
+    apply ex_intro with (x := Add U x0 x1).
+    split; [ split; [ try assumption | idtac ] | idtac ].
+    apply card_add; auto with sets.
+    red in |- *; intro H'9; try exact H'9.
+    apply H'1.
+    elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
+    elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
+    red in |- *; auto with sets.
+    intros x2 H'4; elim H'4; auto with sets.
+    intros x3 H'11; elim H'11; auto with sets.
+    elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
+    apply Im_add; auto with sets.
+  Qed.
+
+  Theorem Image_set_continuous' :
+    forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+      Approximant V (Im U V A f) X ->
+      exists Y : _, Approximant U A Y /\ Im U V Y f = X.
+  Proof.
+    intros A f X H'; try assumption.
+    cut
+      (exists n : _,
+	(exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
+    intro H'0; elim H'0; intros n E; elim E; clear H'0.
+    intros x H'0; try assumption.
+    elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
+      clear H'1 H'0; auto with sets.
+    exists x.
+    split; [ idtac | try assumption ].
+    apply Defn_of_Approximant; auto with sets.
+    apply cardinal_finite with (n := n); auto with sets.
+    apply Image_set_continuous; auto with sets.
+    elim H'; auto with sets.
+    elim H'; auto with sets.
+  Qed.
+
+  Theorem Pigeonhole_bis :
+    forall (A:Ensemble U) (f:U -> V),
+      ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
+  Proof.
+    intros A f H'0 H'1; try assumption.
+    elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
+    intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+    elim (make_new_approximant A x); auto with sets.
+    intros x0 H'2; elim H'2.
+    intros H'5 H'6.
+    elim (finite_cardinal V (Im U V A f)); auto with sets.
+    intros n E.
+    elim (finite_cardinal U x); auto with sets.
+    intros n0 E0.
+    apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
+    apply card_add; auto with sets.
+    rewrite (Im_add U V x x0 f); auto with sets.
+    cut (In V (Im U V x f) (f x0)).
+    intro H'8.
+    rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
+    rewrite H'4; auto with sets.
+    elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
+    apply le_lt_n_Sm.
+    apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
+      auto with sets.
+    rewrite H'4; auto with sets.
+    elim H'3; auto with sets.
+  Qed.
+  
+  Theorem Pigeonhole_ter :
+    forall (A:Ensemble U) (f:U -> V) (n:nat),
+      injective U V f -> Finite V (Im U V A f) -> Finite U A.
+  Proof.
+    intros A f H' H'0 H'1.
+    apply NNPP.
+    red in |- *; intro H'2.
+    elim (Pigeonhole_bis A f); auto with sets.
+  Qed.
 
 End Infinite_sets.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 970d6dab1..88cdabe3f 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -45,120 +45,117 @@ Require Export Partial_Order.
 Require Export Cpo.
 
 Section Integers_sect.
-
-Inductive Integers : Ensemble nat :=
+  
+  Inductive Integers : Ensemble nat :=
     Integers_defn : forall x:nat, In nat Integers x.
-Hint Resolve Integers_defn.
-
-Lemma le_reflexive : Reflexive nat le.
-Proof.
-red in |- *; auto with arith.
-Qed.
-
-Lemma le_antisym : Antisymmetric nat le.
-Proof.
-red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
-Qed.
-
-Lemma le_trans : Transitive nat le.
-Proof.
-red in |- *; intros; apply le_trans with y; auto.
-Qed.
-Hint Resolve le_reflexive le_antisym le_trans.
-
-Lemma le_Order : Order nat le.
-Proof.
-auto with sets arith.
-Qed.
-Hint Resolve le_Order.
-
-Lemma triv_nat : forall n:nat, In nat Integers n.
-Proof.
-auto with sets arith.
-Qed.
-Hint Resolve triv_nat.
-
-Definition nat_po : PO nat.
-apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
- auto with sets arith.
-apply Inhabited_intro with (x := 0); auto with sets arith.
-Defined.
-Hint Unfold nat_po.
-
-Lemma le_total_order : Totally_ordered nat nat_po Integers.
-Proof.
-apply Totally_ordered_definition.
-simpl in |- *.
-intros H' x y H'0.
-specialize  2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
-intro H'1; left; auto with sets arith.
-intro H'1; right.
-cut (y <= x); auto with sets arith.
-Qed.
-Hint Resolve le_total_order.
-
-Lemma Finite_subset_has_lub :
- forall X:Ensemble nat,
-   Finite nat X ->  exists m : nat, Upper_Bound nat nat_po X m.
-Proof.
-intros X H'; elim H'.
-exists 0.
-apply Upper_Bound_definition; auto with sets arith.
-intros y H'0; elim H'0; auto with sets arith.
-intros A H'0 H'1 x H'2; try assumption.
-elim H'1; intros x0 H'3; clear H'1.
-elim le_total_order.
-simpl in |- *.
-intro H'1; try assumption.
-lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.
-generalize (H'4 x0 x).
-clear H'4.
-clear H'1.
-intro H'1; lapply H'1;
- [ intro H'4; elim H'4;
-    [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
- | clear H'1 ].
-exists x.
-apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
-intros y H'1; elim H'1.
-generalize le_trans.
-intro H'4; red in H'4.
-intros x1 H'6; try assumption.
-apply H'4 with (y := x0); auto with sets arith.
-elim H'3; simpl in |- *; auto with sets arith.
-intros x1 H'4; elim H'4; auto with sets arith.
-exists x0.
-apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
-intros y H'1; elim H'1.
-intros x1 H'4; try assumption.
-elim H'3; simpl in |- *; auto with sets arith.
-intros x1 H'4; elim H'4; auto with sets arith.
-red in |- *.
-intros x1 H'1; elim H'1; auto with sets arith.
-Qed.
-
-Lemma Integers_has_no_ub :
- ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
-Proof.
-red in |- *; intro H'; elim H'.
-intros x H'0.
-elim H'0; intros H'1 H'2.
-cut (In nat Integers (S x)).
-intro H'3.
-specialize  1H'2 with (y := S x); intro H'4; lapply H'4;
- [ intro H'5; clear H'4 | try assumption; clear H'4 ].
-simpl in H'5.
-absurd (S x <= x); auto with arith.
-auto with sets arith.
-Qed.
 
-Lemma Integers_infinite : ~ Finite nat Integers.
-Proof.
-generalize Integers_has_no_ub.
-intro H'; red in |- *; intro H'0; try exact H'0.
-apply H'.
-apply Finite_subset_has_lub; auto with sets arith.
-Qed.
+  Lemma le_reflexive : Reflexive nat le.
+  Proof.
+    red in |- *; auto with arith.
+  Qed.
+  
+  Lemma le_antisym : Antisymmetric nat le.
+  Proof.
+    red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
+  Qed.
+
+  Lemma le_trans : Transitive nat le.
+  Proof.
+    red in |- *; intros; apply le_trans with y; auto.
+  Qed.
+  
+  Lemma le_Order : Order nat le.
+  Proof.
+    split; [exact le_reflexive | exact le_trans | exact le_antisym]. 
+  Qed.
+  
+  Lemma triv_nat : forall n:nat, In nat Integers n.
+  Proof.
+    exact Integers_defn.
+  Qed.
+
+  Definition nat_po : PO nat.
+    apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
+      auto with sets arith.
+    apply Inhabited_intro with (x := 0). 
+      apply Integers_defn.
+      exact le_Order.
+  Defined.
+  
+  Lemma le_total_order : Totally_ordered nat nat_po Integers.
+  Proof.
+    apply Totally_ordered_definition.
+    simpl in |- *.
+    intros H' x y H'0.
+    specialize  2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+    intro H'1; left; auto with sets arith.
+    intro H'1; right.
+    cut (y <= x); auto with sets arith.
+  Qed.
+  
+  Lemma Finite_subset_has_lub :
+    forall X:Ensemble nat,
+      Finite nat X ->  exists m : nat, Upper_Bound nat nat_po X m.
+  Proof.
+    intros X H'; elim H'.
+    exists 0.
+    apply Upper_Bound_definition.
+      unfold nat_po. simpl. apply triv_nat.
+    intros y H'0; elim H'0; auto with sets arith.
+    intros A H'0 H'1 x H'2; try assumption.
+    elim H'1; intros x0 H'3; clear H'1.
+    elim le_total_order.
+    simpl in |- *.
+    intro H'1; try assumption.
+    lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.
+    generalize (H'4 x0 x).
+    clear H'4.
+    clear H'1.
+    intro H'1; lapply H'1;
+      [ intro H'4; elim H'4;
+	[ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
+	| clear H'1 ].
+    exists x.
+    apply Upper_Bound_definition. simpl in |- *. apply triv_nat.
+    intros y H'1; elim H'1.
+    generalize le_trans.
+    intro H'4; red in H'4.
+    intros x1 H'6; try assumption.
+    apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial.
+    intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial.
+    exists x0.
+    apply Upper_Bound_definition. 
+      unfold nat_po. simpl. apply triv_nat.
+    intros y H'1; elim H'1.
+    intros x1 H'4; try assumption.
+    elim H'3; simpl in |- *; auto with sets arith.
+    intros x1 H'4; elim H'4; auto with sets arith.
+    red in |- *.
+    intros x1 H'1; elim H'1; apply triv_nat.
+  Qed.
+
+  Lemma Integers_has_no_ub :
+    ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
+  Proof.
+    red in |- *; intro H'; elim H'.
+    intros x H'0.
+    elim H'0; intros H'1 H'2.
+    cut (In nat Integers (S x)).
+    intro H'3.
+    specialize  1H'2 with (y := S x); intro H'4; lapply H'4;
+      [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+    simpl in H'5.
+    absurd (S x <= x); auto with arith.
+    apply triv_nat.
+ Qed.
+  
+  Lemma Integers_infinite : ~ Finite nat Integers.
+  Proof.
+    generalize Integers_has_no_ub.
+    intro H'; red in |- *; intro H'0; try exact H'0.
+    apply H'.
+    apply Finite_subset_has_lub; auto with sets arith.
+  Qed.
 
 End Integers_sect.
 
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index aad294e93..80491c0aa 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -16,162 +16,156 @@ Set Implicit Arguments.
 
 Section multiset_defs.
 
-Variable A : Set.
-Variable eqA : A -> A -> Prop.
-Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+  Variable A : Set.
+  Variable eqA : A -> A -> Prop.
+  Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
-Inductive multiset : Set :=
+  Inductive multiset : Set :=
     Bag : (A -> nat) -> multiset.
-
-Definition EmptyBag := Bag (fun a:A => 0).
-Definition SingletonBag (a:A) :=
-  Bag (fun a':A => match Aeq_dec a a' with
-                   | left _ => 1
-                   | right _ => 0
-                   end).
-
-Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
-
-(** multiset equality *)
-Definition meq (m1 m2:multiset) :=
-  forall a:A, multiplicity m1 a = multiplicity m2 a.
-
-Hint Unfold meq multiplicity.
-
-Lemma meq_refl : forall x:multiset, meq x x.
-Proof.
-destruct x; auto.
-Qed.
-Hint Resolve meq_refl.
-
-Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
-Proof.
-unfold meq in |- *.
-destruct x; destruct y; destruct z.
-intros; rewrite H; auto.
-Qed.
-
-Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
-Proof.
-unfold meq in |- *.
-destruct x; destruct y; auto.
-Qed.
-Hint Immediate meq_sym.
-
-(** multiset union *)
-Definition munion (m1 m2:multiset) :=
-  Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).
-
-Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
-Proof.
-unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
-Qed.
-Hint Resolve munion_empty_left.
-
-Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
-Proof.
-unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
-Qed.
-
-
-Require Import Plus. (* comm. and ass. of plus *)
-
-Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
-Proof.
-unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
-destruct x; destruct y; auto with arith.
-Qed.
-Hint Resolve munion_comm.
-
-Lemma munion_ass :
- forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
-Proof.
-unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
-destruct x; destruct y; destruct z; auto with arith.
-Qed.
-Hint Resolve munion_ass.
-
-Lemma meq_left :
- forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
-Proof.
-unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
-destruct x; destruct y; destruct z.
-intros; elim H; auto with arith.
-Qed.
-Hint Resolve meq_left.
-
-Lemma meq_right :
- forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
-Proof.
-unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
-destruct x; destruct y; destruct z.
-intros; elim H; auto.
-Qed.
-Hint Resolve meq_right.
-
-
-(** Here we should make multiset an abstract datatype, by hiding [Bag],
-    [munion], [multiplicity]; all further properties are proved abstractly *)
-
-Lemma munion_rotate :
- forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
-Proof.
-intros; apply (op_rotate multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma meq_congr :
- forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
-Proof.
-intros; apply (cong_congr multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma munion_perm_left :
- forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
-Proof.
-intros; apply (perm_left multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma multiset_twist1 :
- forall x y z t:multiset,
-   meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
-Proof.
-intros; apply (twist multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma multiset_twist2 :
- forall x y z t:multiset,
-   meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
-Proof.
-intros; apply meq_trans with (munion (munion x (munion y z)) t).
-apply meq_sym; apply munion_ass.
-apply meq_left; apply munion_perm_left.
-Qed.
-
-(** specific for treesort *)
-
-Lemma treesort_twist1 :
- forall x y z t u:multiset,
-   meq u (munion y z) ->
-   meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
-Proof.
-intros; apply meq_trans with (munion x (munion (munion y z) t)).
-apply meq_right; apply meq_left; trivial.
-apply multiset_twist1.
-Qed.
-
-Lemma treesort_twist2 :
- forall x y z t u:multiset,
-   meq u (munion y z) ->
-   meq (munion x (munion u t)) (munion (munion y (munion x z)) t).
-Proof.
-intros; apply meq_trans with (munion x (munion (munion y z) t)).
-apply meq_right; apply meq_left; trivial.
-apply multiset_twist2.
-Qed.
+  
+  Definition EmptyBag := Bag (fun a:A => 0).
+  Definition SingletonBag (a:A) :=
+    Bag (fun a':A => match Aeq_dec a a' with
+                       | left _ => 1
+                       | right _ => 0
+                     end).
+
+  Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
+  
+  (** multiset equality *)
+  Definition meq (m1 m2:multiset) :=
+    forall a:A, multiplicity m1 a = multiplicity m2 a.
+  
+  Lemma meq_refl : forall x:multiset, meq x x.
+  Proof.
+    destruct x; unfold meq; reflexivity.
+  Qed.
+  
+  Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
+  Proof.
+    unfold meq in |- *.
+    destruct x; destruct y; destruct z.
+    intros; rewrite H; auto.
+  Qed.
+  
+  Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
+  Proof.
+    unfold meq in |- *.
+    destruct x; destruct y; auto.
+  Qed.
+
+  (** multiset union *)
+  Definition munion (m1 m2:multiset) :=
+    Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).
+
+  Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
+  Proof.
+    unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+  Qed.
+  
+  Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
+  Proof.
+    unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+  Qed.
+
+
+  Require Plus. (* comm. and ass. of plus *)
+  
+  Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
+  Proof.
+    unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
+    destruct x; destruct y; auto with arith.
+  Qed.
+
+  Lemma munion_ass :
+    forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
+  Proof.
+    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+    destruct x; destruct y; destruct z; auto with arith.
+  Qed.
+
+  Lemma meq_left :
+    forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
+  Proof.
+    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+    destruct x; destruct y; destruct z.
+    intros; elim H; auto with arith.
+  Qed.
+
+  Lemma meq_right :
+    forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
+  Proof.
+    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+    destruct x; destruct y; destruct z.
+    intros; elim H; auto.
+  Qed.
+
+  (** Here we should make multiset an abstract datatype, by hiding [Bag],
+      [munion], [multiplicity]; all further properties are proved abstractly *)
+
+  Lemma munion_rotate :
+    forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
+  Proof.
+    intros; apply (op_rotate multiset munion meq). 
+      apply munion_comm.
+      apply munion_ass.
+      exact meq_trans.
+      exact meq_sym.
+      trivial.
+  Qed.
+  
+  Lemma meq_congr :
+    forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
+  Proof.
+    intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right.
+      exact meq_trans.
+  Qed.
+  
+  Lemma munion_perm_left :
+    forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
+  Proof.
+    intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym.
+      exact meq_trans.
+  Qed.
+  
+  Lemma multiset_twist1 :
+    forall x y z t:multiset,
+      meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
+  Proof.
+    intros; apply (twist multiset munion meq); auto using munion_comm, munion_ass, meq_sym, meq_left, meq_right.
+    exact meq_trans.
+  Qed.
+
+  Lemma multiset_twist2 :
+    forall x y z t:multiset,
+      meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
+  Proof.
+    intros; apply meq_trans with (munion (munion x (munion y z)) t).
+    apply meq_sym; apply munion_ass.
+    apply meq_left; apply munion_perm_left.
+  Qed.
+
+  (** specific for treesort *)
+
+  Lemma treesort_twist1 :
+    forall x y z t u:multiset,
+      meq u (munion y z) ->
+      meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
+  Proof.
+    intros; apply meq_trans with (munion x (munion (munion y z) t)).
+    apply meq_right; apply meq_left; trivial.
+    apply multiset_twist1.
+  Qed.
+  
+  Lemma treesort_twist2 :
+    forall x y z t u:multiset,
+      meq u (munion y z) ->
+      meq (munion x (munion u t)) (munion (munion y (munion x z)) t).
+  Proof.
+    intros; apply meq_trans with (munion x (munion (munion y z) t)).
+    apply meq_right; apply meq_left; trivial.
+    apply multiset_twist2.
+  Qed.
 
 
 (*i theory of minter to do similarly 
@@ -188,4 +182,4 @@ Unset Implicit Arguments.
 Hint Unfold meq multiplicity: v62 datatypes.
 Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
   munion_empty_left: v62 datatypes.
-Hint Immediate meq_sym: v62 datatypes.
\ No newline at end of file
+Hint Immediate meq_sym: v62 datatypes.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 07244e66f..8589f387e 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -30,26 +30,26 @@ Require Export Ensembles.
 Require Export Relations_1.
 
 Section Partial_orders.
-Variable U : Type.
-
-Definition Carrier := Ensemble U.
-
-Definition Rel := Relation U.
-
-Record PO : Type := Definition_of_PO
-  {Carrier_of : Ensemble U;
-   Rel_of : Relation U;
-   PO_cond1 : Inhabited U Carrier_of;
-   PO_cond2 : Order U Rel_of}.
-Variable p : PO.
-
-Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
-
-Inductive covers (y x:U) : Prop :=
+  Variable U : Type.
+  
+  Definition Carrier := Ensemble U.
+  
+  Definition Rel := Relation U.
+  
+  Record PO : Type := Definition_of_PO
+    { Carrier_of : Ensemble U;
+      Rel_of : Relation U;
+      PO_cond1 : Inhabited U Carrier_of;
+      PO_cond2 : Order U Rel_of }.
+  Variable p : PO.
+  
+  Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
+  
+  Inductive covers (y x:U) : Prop :=
     Definition_of_covers :
-      Strict_Rel_of x y ->
-      ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) ->
-      covers y x.
+    Strict_Rel_of x y ->
+    ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) ->
+    covers y x.
 
 End Partial_orders.
 
@@ -58,43 +58,45 @@ Hint Resolve Definition_of_covers: sets v62.
 
 
 Section Partial_order_facts.
-Variable U : Type.
-Variable D : PO U.
-
-Lemma Strict_Rel_Transitive_with_Rel :
- forall x y z:U,
-   Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
-unfold Strict_Rel_of at 1 in |- *.
-red in |- *.
-elim D; simpl in |- *.
-intros C R H' H'0; elim H'0.
-intros H'1 H'2 H'3 x y z H'4 H'5; split.
-apply H'2 with (y := y); tauto.
-red in |- *; intro H'6.
-elim H'4; intros H'7 H'8; apply H'8; clear H'4.
-apply H'3; auto.
-rewrite H'6; tauto.
-Qed.
+  Variable U : Type.
+  Variable D : PO U.
+  
+  Lemma Strict_Rel_Transitive_with_Rel :
+    forall x y z:U,
+      Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
+  Proof.
+    unfold Strict_Rel_of at 1 in |- *.
+    red in |- *.
+    elim D; simpl in |- *.
+    intros C R H' H'0; elim H'0.
+    intros H'1 H'2 H'3 x y z H'4 H'5; split.
+    apply H'2 with (y := y); tauto.
+    red in |- *; intro H'6.
+    elim H'4; intros H'7 H'8; apply H'8; clear H'4.
+    apply H'3; auto.
+    rewrite H'6; tauto.
+  Qed.
 
-Lemma Strict_Rel_Transitive_with_Rel_left :
- forall x y z:U,
-   Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
-unfold Strict_Rel_of at 1 in |- *.
-red in |- *.
-elim D; simpl in |- *.
-intros C R H' H'0; elim H'0.
-intros H'1 H'2 H'3 x y z H'4 H'5; split.
-apply H'2 with (y := y); tauto.
-red in |- *; intro H'6.
-elim H'5; intros H'7 H'8; apply H'8; clear H'5.
-apply H'3; auto.
-rewrite <- H'6; auto.
-Qed.
+  Lemma Strict_Rel_Transitive_with_Rel_left :
+    forall x y z:U,
+      Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
+  Proof.
+    unfold Strict_Rel_of at 1 in |- *.
+    red in |- *.
+    elim D; simpl in |- *.
+    intros C R H' H'0; elim H'0.
+    intros H'1 H'2 H'3 x y z H'4 H'5; split.
+    apply H'2 with (y := y); tauto.
+    red in |- *; intro H'6.
+    elim H'5; intros H'7 H'8; apply H'8; clear H'5.
+    apply H'3; auto.
+    rewrite <- H'6; auto.
+  Qed.
 
-Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
-red in |- *.
-intros x y z H' H'0.
-apply Strict_Rel_Transitive_with_Rel with (y := y);
- [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
-Qed.
+  Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
+    red in |- *.
+    intros x y z H' H'0.
+    apply Strict_Rel_Transitive_with_Rel with (y := y);
+      [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
+  Qed.
 End Partial_order_facts.
\ No newline at end of file
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 006831909..7c6b551c6 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -15,77 +15,75 @@
 
 Section Axiomatisation.
 
-Variable U : Set.
-
-Variable op : U -> U -> U.
-
-Variable cong : U -> U -> Prop.
-
-Hypothesis op_comm : forall x y:U, cong (op x y) (op y x).
-Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)).
-
-Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z).
-Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y).
-Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z.
-Hypothesis cong_sym : forall x y:U, cong x y -> cong y x.
-
-(** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
-
-Lemma cong_congr :
- forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).
-Proof.
-intros; apply cong_trans with (op y z).
-apply cong_left; trivial.
-apply cong_right; trivial.
-Qed.
-
-Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
-Proof.
-intros; apply cong_right; apply op_comm.
-Qed.
-
-Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z).
-Proof.
-intros; apply cong_left; apply op_comm.
-Qed.
-
-Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
-Proof.
-intros.
-apply cong_trans with (op x (op y z)).
-apply op_ass.
-apply cong_trans with (op x (op z y)). 
-apply cong_right; apply op_comm.
-apply cong_sym; apply op_ass.
-Qed.
-
-Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
-Proof.
-intros.
-apply cong_trans with (op (op x y) z).
-apply cong_sym; apply op_ass.
-apply cong_trans with (op (op y x) z).
-apply cong_left; apply op_comm.
-apply op_ass.
-Qed.
-
-Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
-Proof.
-intros; apply cong_trans with (op (op x y) z).
-apply cong_sym; apply op_ass.
-apply op_comm.
-Qed.
-
-(* Needed for treesort ... *)
-Lemma twist :
- forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).
-Proof.
-intros.
-apply cong_trans with (op x (op (op y t) z)).
-apply cong_right; apply perm_right.
-apply cong_trans with (op (op x (op y t)) z).
-apply cong_sym; apply op_ass.
-apply cong_left; apply perm_left.
-Qed.
+  Variable U : Set.
+  Variable op : U -> U -> U.
+  Variable cong : U -> U -> Prop.
+
+  Hypothesis op_comm : forall x y:U, cong (op x y) (op y x).
+  Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)).
+
+  Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z).
+  Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y).
+  Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z.
+  Hypothesis cong_sym : forall x y:U, cong x y -> cong y x.
+
+  (** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
+
+  Lemma cong_congr :
+    forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).
+  Proof.
+    intros; apply cong_trans with (op y z).
+    apply cong_left; trivial.
+    apply cong_right; trivial.
+  Qed.
+  
+  Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
+  Proof.
+    intros; apply cong_right; apply op_comm.
+  Qed.
+  
+  Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z).
+  Proof.
+    intros; apply cong_left; apply op_comm.
+  Qed.
+  
+  Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
+  Proof.
+    intros.
+    apply cong_trans with (op x (op y z)).
+    apply op_ass.
+    apply cong_trans with (op x (op z y)). 
+    apply cong_right; apply op_comm.
+    apply cong_sym; apply op_ass.
+  Qed.
+
+  Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
+  Proof.
+    intros.
+    apply cong_trans with (op (op x y) z).
+    apply cong_sym; apply op_ass.
+    apply cong_trans with (op (op y x) z).
+    apply cong_left; apply op_comm.
+    apply op_ass.
+  Qed.
+  
+  Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
+  Proof.
+    intros; apply cong_trans with (op (op x y) z).
+    apply cong_sym; apply op_ass.
+    apply op_comm.
+  Qed.
+
+  (** Needed for treesort ... *)
+  Lemma twist :
+    forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).
+  Proof.
+    intros.
+    apply cong_trans with (op x (op (op y t) z)).
+    apply cong_right; apply perm_right.
+    apply cong_trans with (op (op x (op y t)) z).
+    apply cong_sym; apply op_ass.
+    apply cong_left; apply perm_left.
+  Qed.
 
 End Axiomatisation.
\ No newline at end of file
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 1ac59056b..8116045b6 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -39,298 +39,294 @@ Require Export Classical_sets.
 
 Section Sets_as_an_algebra.
 
-Variable U : Type.
+  Variable U : Type.
+  
+  Lemma sincl_add_x :
+    forall (A B:Ensemble U) (x:U),
+      ~ In U A x ->
+      Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
+  Proof.
+    intros A B x H' H'0; red in |- *.
+    lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
+    clear H'0; intro H'0; split.
+    apply incl_add_x with (x := x); tauto.
+    elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
+    intros x0 H'0.
+    red in |- *; intro H'2.
+    elim H'0; clear H'0.
+    rewrite <- H'2; auto with sets.
+  Qed.
 
-Lemma sincl_add_x :
- forall (A B:Ensemble U) (x:U),
-   ~ In U A x ->
-   Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
-Proof.
-intros A B x H' H'0; red in |- *.
-lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
-clear H'0; intro H'0; split.
-apply incl_add_x with (x := x); tauto.
-elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
-intros x0 H'0.
-red in |- *; intro H'2.
-elim H'0; clear H'0.
-rewrite <- H'2; auto with sets.
-Qed.
+  Lemma incl_soustr_in :
+    forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
+  Proof.
+    intros X x H'; red in |- *.
+    intros x0 H'0; elim H'0; auto with sets.
+  Qed.
+  
+  Lemma incl_soustr :
+    forall (X Y:Ensemble U) (x:U),
+      Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
+  Proof.
+    intros X Y x H'; red in |- *.
+    intros x0 H'0; elim H'0.
+    intros H'1 H'2.
+    apply Subtract_intro; auto with sets.
+  Qed.
+  
+  Lemma incl_soustr_add_l :
+    forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
+  Proof.
+    intros X x; red in |- *.
+    intros x0 H'; elim H'; auto with sets.
+    intro H'0; elim H'0; auto with sets.
+    intros t H'1 H'2; elim H'2; auto with sets.
+  Qed.
 
-Lemma incl_soustr_in :
- forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; elim H'0; auto with sets.
-Qed.
-Hint Resolve incl_soustr_in: sets v62.
-
-Lemma incl_soustr :
- forall (X Y:Ensemble U) (x:U),
-   Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
-Proof.
-intros X Y x H'; red in |- *.
-intros x0 H'0; elim H'0.
-intros H'1 H'2.
-apply Subtract_intro; auto with sets.
-Qed.
-Hint Resolve incl_soustr: sets v62.
-
-
-Lemma incl_soustr_add_l :
- forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
-Proof.
-intros X x; red in |- *.
-intros x0 H'; elim H'; auto with sets.
-intro H'0; elim H'0; auto with sets.
-intros t H'1 H'2; elim H'2; auto with sets.
-Qed.
-Hint Resolve incl_soustr_add_l: sets v62.
+  Lemma incl_soustr_add_r :
+    forall (X:Ensemble U) (x:U),
+      ~ In U X x -> Included U X (Subtract U (Add U X x) x).
+  Proof.
+    intros X x H'; red in |- *.
+    intros x0 H'0; try assumption.
+    apply Subtract_intro; auto with sets.
+    red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
+  Qed.
+  Hint Resolve incl_soustr_add_r: sets v62.
+  
+  Lemma add_soustr_2 :
+    forall (X:Ensemble U) (x:U),
+      In U X x -> Included U X (Add U (Subtract U X x) x).
+  Proof.
+    intros X x H'; red in |- *.
+    intros x0 H'0; try assumption.
+    elim (classic (x = x0)); intro K; auto with sets.
+    elim K; auto with sets.
+  Qed.
+  
+  Lemma add_soustr_1 :
+    forall (X:Ensemble U) (x:U),
+      In U X x -> Included U (Add U (Subtract U X x) x) X.
+  Proof.
+    intros X x H'; red in |- *.
+    intros x0 H'0; elim H'0; auto with sets.
+    intros y H'1; elim H'1; auto with sets.
+    intros t H'1; try assumption.
+    rewrite <- (Singleton_inv U x t); auto with sets.
+  Qed.
+  
+  Lemma add_soustr_xy :
+    forall (X:Ensemble U) (x y:U),
+      x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
+  Proof.
+    intros X x y H'; apply Extensionality_Ensembles.
+    split; red in |- *.
+    intros x0 H'0; elim H'0; auto with sets.
+    intro H'1; elim H'1.
+    intros u H'2 H'3; try assumption.
+    apply Add_intro1.
+    apply Subtract_intro; auto with sets.
+    intros t H'2 H'3; try assumption.
+    elim (Singleton_inv U x t); auto with sets.
+    intros u H'2; try assumption.
+    elim (Add_inv U (Subtract U X y) x u); auto with sets.
+    intro H'0; elim H'0; auto with sets.
+    intro H'0; rewrite <- H'0; auto with sets.
+  Qed.
+  
+  Lemma incl_st_add_soustr :
+    forall (X Y:Ensemble U) (x:U),
+      ~ In U X x ->
+      Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
+  Proof.
+    intros X Y x H' H'0; apply sincl_add_x with (x := x); auto using add_soustr_1 with sets.
+    split.
+    elim H'0.
+    intros H'1 H'2.
+    generalize (Inclusion_is_transitive U).
+    intro H'4; red in H'4.
+    apply H'4 with (y := Y); auto using add_soustr_2 with sets.
+    red in H'0.
+    elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
+    red in |- *; intro H'0; apply H'2.
+    rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
+  Qed.
+  
+  Lemma Sub_Add_new :
+    forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
+  Proof.
+    auto using incl_soustr_add_l with sets.
+  Qed.
+  
+  Lemma Simplify_add :
+    forall (X X0:Ensemble U) (x:U),
+      ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
+  Proof.
+    intros X X0 x H' H'0 H'1; try assumption.
+    rewrite (Sub_Add_new X x); auto with sets.
+    rewrite (Sub_Add_new X0 x); auto with sets.
+    rewrite H'1; auto with sets.
+  Qed.
+  
+  Lemma Included_Add :
+    forall (X A:Ensemble U) (x:U),
+      Included U X (Add U A x) ->
+      Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
+  Proof.
+    intros X A x H'0; try assumption.
+    elim (classic (In U X x)).
+    intro H'1; right; try assumption.
+    exists (Subtract U X x).
+    split; auto using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
+    red in H'0.
+    red in |- *.
+    intros x0 H'2; try assumption.
+    lapply (Subtract_inv U X x x0); auto with sets.
+    intro H'3; elim H'3; intros K K'; clear H'3.
+    lapply (H'0 x0); auto with sets.
+    intro H'3; try assumption.
+    lapply (Add_inv U A x x0); auto with sets.
+    intro H'4; elim H'4;
+      [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+    elim K'; auto with sets.
+    intro H'1; left; try assumption.
+    red in H'0.
+    red in |- *.
+    intros x0 H'2; try assumption.
+    lapply (H'0 x0); auto with sets.
+    intro H'3; try assumption.
+    lapply (Add_inv U A x x0); auto with sets.
+    intro H'4; elim H'4;
+      [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+    absurd (In U X x0); auto with sets.
+    rewrite <- H'5; auto with sets.
+  Qed.
+  
+  Lemma setcover_inv :
+    forall A x y:Ensemble U,
+      covers (Ensemble U) (Power_set_PO U A) y x ->
+      Strict_Included U x y /\
+      (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
+  Proof.
+    intros A x y H'; elim H'.
+    unfold Strict_Rel_of in |- *; simpl in |- *.
+    intros H'0 H'1; split; [ auto with sets | idtac ].
+    intros z H'2 H'3; try assumption.
+    elim (classic (x = z)); auto with sets.
+    intro H'4; right; try assumption.
+    elim (classic (z = y)); auto with sets.
+    intro H'5; try assumption.
+    elim H'1.
+    exists z; auto with sets.
+  Qed.
+  
+  Theorem Add_covers :
+    forall A a:Ensemble U,
+      Included U a A ->
+      forall x:U,
+	In U A x ->
+	~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
+  Proof.
+    intros A a H' x H'0 H'1; try assumption.
+    apply setcover_intro; auto with sets.
+    red in |- *.
+    split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
+    apply H'1.
+    rewrite H'2; auto with sets.
+    red in |- *; intro H'2; elim H'2; clear H'2.
+    intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+    lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
+    intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
+    intros x0 H'2; elim H'2.
+    intros H'5 H'6; try assumption.
+    generalize H'4; intro K.
+    red in H'4.
+    elim H'4; intros H'8 H'9; red in H'8; clear H'4.
+    lapply (H'8 x0); auto with sets.
+    intro H'7; try assumption.
+    elim (Add_inv U a x x0); auto with sets.
+    intro H'15.
+    cut (Included U (Add U a x) z).
+    intro H'10; try assumption.
+    red in K.
+    elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
+    rewrite H'15.
+    red in |- *.
+    intros x1 H'10; elim H'10; auto with sets.
+    intros x2 H'11; elim H'11; auto with sets.
+  Qed.
+  
+  Theorem covers_Add :
+    forall A a a':Ensemble U,
+      Included U a A ->
+      Included U a' A ->
+      covers (Ensemble U) (Power_set_PO U A) a' a ->
+      exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.
+  Proof.
+    intros A a a' H' H'0 H'1; try assumption.
+    elim (setcover_inv A a a'); auto with sets.
+    intros H'6 H'7.
+    clear H'1.
+    elim (Strict_Included_inv U a a'); auto with sets.
+    intros H'5 H'8; elim H'8.
+    intros x H'1; elim H'1.
+    intros H'2 H'3; try assumption.
+    exists x.
+    split; [ try assumption | idtac ].
+    clear H'8 H'1.
+    elim (H'7 (Add U a x)); auto with sets.
+    intro H'1.
+    absurd (a = Add U a x); auto with sets.
+    red in |- *; intro H'8; try exact H'8.
+    apply H'3.
+    rewrite H'8; auto with sets.
+    auto with sets.
+    red in |- *.
+    intros x0 H'1; elim H'1; auto with sets.
+    intros x1 H'8; elim H'8; auto with sets.
+    split; [ idtac | try assumption ].
+    red in H'0; auto with sets.
+  Qed.
 
-Lemma incl_soustr_add_r :
- forall (X:Ensemble U) (x:U),
-   ~ In U X x -> Included U X (Subtract U (Add U X x) x).
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; try assumption.
-apply Subtract_intro; auto with sets.
-red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
-Qed.
-Hint Resolve incl_soustr_add_r: sets v62.
-
-Lemma add_soustr_2 :
- forall (X:Ensemble U) (x:U),
-   In U X x -> Included U X (Add U (Subtract U X x) x).
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; try assumption.
-elim (classic (x = x0)); intro K; auto with sets.
-elim K; auto with sets.
-Qed.
-
-Lemma add_soustr_1 :
- forall (X:Ensemble U) (x:U),
-   In U X x -> Included U (Add U (Subtract U X x) x) X.
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; elim H'0; auto with sets.
-intros y H'1; elim H'1; auto with sets.
-intros t H'1; try assumption.
-rewrite <- (Singleton_inv U x t); auto with sets.
-Qed.
-Hint Resolve add_soustr_1 add_soustr_2: sets v62.
-
-Lemma add_soustr_xy :
- forall (X:Ensemble U) (x y:U),
-   x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
-Proof.
-intros X x y H'; apply Extensionality_Ensembles.
-split; red in |- *.
-intros x0 H'0; elim H'0; auto with sets.
-intro H'1; elim H'1.
-intros u H'2 H'3; try assumption.
-apply Add_intro1.
-apply Subtract_intro; auto with sets.
-intros t H'2 H'3; try assumption.
-elim (Singleton_inv U x t); auto with sets.
-intros u H'2; try assumption.
-elim (Add_inv U (Subtract U X y) x u); auto with sets.
-intro H'0; elim H'0; auto with sets.
-intro H'0; rewrite <- H'0; auto with sets.
-Qed.
-Hint Resolve add_soustr_xy: sets v62.
-
-Lemma incl_st_add_soustr :
- forall (X Y:Ensemble U) (x:U),
-   ~ In U X x ->
-   Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
-Proof.
-intros X Y x H' H'0; apply sincl_add_x with (x := x); auto with sets.
-split.
-elim H'0.
-intros H'1 H'2.
-generalize (Inclusion_is_transitive U).
-intro H'4; red in H'4.
-apply H'4 with (y := Y); auto with sets.
-red in H'0.
-elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
-red in |- *; intro H'0; apply H'2.
-rewrite H'0; auto 8 with sets.
-Qed.
-
-Lemma Sub_Add_new :
- forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
-Proof.
-auto with sets.
-Qed.
-
-Lemma Simplify_add :
- forall (X X0:Ensemble U) (x:U),
-   ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
-Proof.
-intros X X0 x H' H'0 H'1; try assumption.
-rewrite (Sub_Add_new X x); auto with sets.
-rewrite (Sub_Add_new X0 x); auto with sets.
-rewrite H'1; auto with sets.
-Qed.
-
-Lemma Included_Add :
- forall (X A:Ensemble U) (x:U),
-   Included U X (Add U A x) ->
-   Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
-Proof.
-intros X A x H'0; try assumption.
-elim (classic (In U X x)).
-intro H'1; right; try assumption.
-exists (Subtract U X x).
-split; auto with sets.
-red in H'0.
-red in |- *.
-intros x0 H'2; try assumption.
-lapply (Subtract_inv U X x x0); auto with sets.
-intro H'3; elim H'3; intros K K'; clear H'3.
-lapply (H'0 x0); auto with sets.
-intro H'3; try assumption.
-lapply (Add_inv U A x x0); auto with sets.
-intro H'4; elim H'4;
- [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
-elim K'; auto with sets.
-intro H'1; left; try assumption.
-red in H'0.
-red in |- *.
-intros x0 H'2; try assumption.
-lapply (H'0 x0); auto with sets.
-intro H'3; try assumption.
-lapply (Add_inv U A x x0); auto with sets.
-intro H'4; elim H'4;
- [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
-absurd (In U X x0); auto with sets.
-rewrite <- H'5; auto with sets.
-Qed.
-
-Lemma setcover_inv :
- forall A x y:Ensemble U,
-   covers (Ensemble U) (Power_set_PO U A) y x ->
-   Strict_Included U x y /\
-   (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
-Proof.
-intros A x y H'; elim H'.
-unfold Strict_Rel_of in |- *; simpl in |- *.
-intros H'0 H'1; split; [ auto with sets | idtac ].
-intros z H'2 H'3; try assumption.
-elim (classic (x = z)); auto with sets.
-intro H'4; right; try assumption.
-elim (classic (z = y)); auto with sets.
-intro H'5; try assumption.
-elim H'1.
-exists z; auto with sets.
-Qed.
-
-Theorem Add_covers :
- forall A a:Ensemble U,
-   Included U a A ->
-   forall x:U,
-     In U A x ->
-     ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
-Proof.
-intros A a H' x H'0 H'1; try assumption.
-apply setcover_intro; auto with sets.
-red in |- *.
-split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
-apply H'1.
-rewrite H'2; auto with sets.
-red in |- *; intro H'2; elim H'2; clear H'2.
-intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
-lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
-intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
-intros x0 H'2; elim H'2.
-intros H'5 H'6; try assumption.
-generalize H'4; intro K.
-red in H'4.
-elim H'4; intros H'8 H'9; red in H'8; clear H'4.
-lapply (H'8 x0); auto with sets.
-intro H'7; try assumption.
-elim (Add_inv U a x x0); auto with sets.
-intro H'15.
-cut (Included U (Add U a x) z).
-intro H'10; try assumption.
-red in K.
-elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
-rewrite H'15.
-red in |- *.
-intros x1 H'10; elim H'10; auto with sets.
-intros x2 H'11; elim H'11; auto with sets.
-Qed.
-
-Theorem covers_Add :
- forall A a a':Ensemble U,
-   Included U a A ->
-   Included U a' A ->
-   covers (Ensemble U) (Power_set_PO U A) a' a ->
-    exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.
-Proof.
-intros A a a' H' H'0 H'1; try assumption.
-elim (setcover_inv A a a'); auto with sets.
-intros H'6 H'7.
-clear H'1.
-elim (Strict_Included_inv U a a'); auto with sets.
-intros H'5 H'8; elim H'8.
-intros x H'1; elim H'1.
-intros H'2 H'3; try assumption.
-exists x.
-split; [ try assumption | idtac ].
-clear H'8 H'1.
-elim (H'7 (Add U a x)); auto with sets.
-intro H'1.
-absurd (a = Add U a x); auto with sets.
-red in |- *; intro H'8; try exact H'8.
-apply H'3.
-rewrite H'8; auto with sets.
-auto with sets.
-red in |- *.
-intros x0 H'1; elim H'1; auto with sets.
-intros x1 H'8; elim H'8; auto with sets.
-split; [ idtac | try assumption ].
-red in H'0; auto with sets.
-Qed.
-
-Theorem covers_is_Add :
- forall A a a':Ensemble U,
-   Included U a A ->
-   Included U a' A ->
-   (covers (Ensemble U) (Power_set_PO U A) a' a <->
-    (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
-Proof.
-intros A a a' H' H'0; split; intro K.
-apply covers_Add with (A := A); auto with sets.
-elim K.
-intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
-apply Add_covers; intuition.
-Qed.
-
-Theorem Singleton_atomic :
- forall (x:U) (A:Ensemble U),
-   In U A x ->
-   covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
-intros x A H'.
-rewrite <- (Empty_set_zero' U x).
-apply Add_covers; auto with sets.
-Qed.
-
-Lemma less_than_singleton :
- forall (X:Ensemble U) (x:U),
-   Strict_Included U X (Singleton U x) -> X = Empty_set U.
-intros X x H'; try assumption.
-red in H'.
-lapply (Singleton_atomic x (Full_set U));
- [ intro H'2; try exact H'2 | apply Full_intro ].
-elim H'; intros H'0 H'1; try exact H'1; clear H'.
-elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
- [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
-elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
- auto with sets.
-elim H'1; auto with sets.
-Qed.
+  Theorem covers_is_Add :
+    forall A a a':Ensemble U,
+      Included U a A ->
+      Included U a' A ->
+      (covers (Ensemble U) (Power_set_PO U A) a' a <->
+	(exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
+  Proof.
+    intros A a a' H' H'0; split; intro K.
+    apply covers_Add with (A := A); auto with sets.
+    elim K.
+    intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
+    apply Add_covers; intuition.
+  Qed.
+  
+  Theorem Singleton_atomic :
+    forall (x:U) (A:Ensemble U),
+      In U A x ->
+      covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
+  Proof.
+    intros x A H'.
+    rewrite <- (Empty_set_zero' U x).
+    apply Add_covers; auto with sets.
+  Qed.
+  
+  Lemma less_than_singleton :
+    forall (X:Ensemble U) (x:U),
+      Strict_Included U X (Singleton U x) -> X = Empty_set U.
+  Proof.
+    intros X x H'; try assumption.
+    red in H'.
+    lapply (Singleton_atomic x (Full_set U));
+      [ intro H'2; try exact H'2 | apply Full_intro ].
+    elim H'; intros H'0 H'1; try exact H'1; clear H'.
+    elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
+      [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
+    elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
+      auto with sets.
+    elim H'1; auto with sets.
+  Qed.
 
 End Sets_as_an_algebra.
 
@@ -339,4 +335,4 @@ Hint Resolve incl_soustr: sets v62.
 Hint Resolve incl_soustr_add_l: sets v62.
 Hint Resolve incl_soustr_add_r: sets v62.
 Hint Resolve add_soustr_1 add_soustr_2: sets v62.
-Hint Resolve add_soustr_xy: sets v62.
\ No newline at end of file
+Hint Resolve add_soustr_xy: sets v62.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index cae796861..dee4af65a 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -35,231 +35,223 @@ Require Export Cpo.
 Require Export Powerset.
 
 Section Sets_as_an_algebra.
-Variable U : Type.
-Hint Unfold not.
+  Variable U : Type.
 
-Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
-Proof.
-auto 6 with sets.
-Qed.
-Hint Resolve Empty_set_zero.
+  Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
+  Proof.
+    auto 6 with sets.
+  Qed.
+  
+  Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
+  Proof.
+    unfold Add at 1 in |- *; auto using Empty_set_zero with sets.
+  Qed.
+  
+  Lemma less_than_empty :
+    forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
+  Proof.
+    auto with sets.
+  Qed.
+  
+  Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
+  Proof.
+    auto with sets.
+  Qed.
+  
+  Theorem Union_associative :
+    forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
+  Proof.
+    auto 9 with sets.
+  Qed.
+  
+  Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
+  Proof.
+    auto 7 with sets.
+  Qed.
+  
+  Lemma Union_absorbs :
+    forall A B:Ensemble U, Included U B A -> Union U A B = A.
+  Proof.
+    auto 7 with sets.
+  Qed.
 
-Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
-Proof.
-unfold Add at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Empty_set_zero'.
+  Theorem Couple_as_union :
+    forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
+  Proof.
+    intros x y; apply Extensionality_Ensembles; split; red in |- *.
+    intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
+    intros x0 H'; elim H'; auto with sets.
+  Qed.
+  
+  Theorem Triple_as_union :
+    forall x y z:U,
+      Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
+      Triple U x y z.
+  Proof.
+    intros x y z; apply Extensionality_Ensembles; split; red in |- *.
+    intros x0 H'; elim H'.
+    intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
+    intros x1 H'0; elim H'0; auto with sets.
+    intros x0 H'; elim H'; auto with sets.
+  Qed.
+  
+  Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
+  Proof.
+    intros x y.
+    rewrite <- (Couple_as_union x y).
+    rewrite <- (Union_idempotent (Singleton U x)).
+    apply Triple_as_union.
+  Qed.
+  
+  Theorem Triple_as_Couple_Singleton :
+    forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
+  Proof.
+    intros x y z.
+    rewrite <- (Triple_as_union x y z).
+    rewrite <- (Couple_as_union x y); auto with sets.
+  Qed.
+  
+  Theorem Intersection_commutative :
+    forall A B:Ensemble U, Intersection U A B = Intersection U B A.
+  Proof.
+    intros A B.
+    apply Extensionality_Ensembles.
+    split; red in |- *; intros x H'; elim H'; auto with sets.
+  Qed.
+  
+  Theorem Distributivity :
+    forall A B C:Ensemble U,
+      Intersection U A (Union U B C) =
+      Union U (Intersection U A B) (Intersection U A C).
+  Proof.
+    intros A B C.
+    apply Extensionality_Ensembles.
+    split; red in |- *; intros x H'.
+    elim H'.
+    intros x0 H'0 H'1; generalize H'0.
+    elim H'1; auto with sets.
+    elim H'; intros x0 H'0; elim H'0; auto with sets.
+  Qed.
+  
+  Theorem Distributivity' :
+    forall A B C:Ensemble U,
+      Union U A (Intersection U B C) =
+      Intersection U (Union U A B) (Union U A C).
+  Proof.
+    intros A B C.
+    apply Extensionality_Ensembles.
+    split; red in |- *; intros x H'.
+    elim H'; auto with sets.
+    intros x0 H'0; elim H'0; auto with sets.
+    elim H'.
+    intros x0 H'0; elim H'0; auto with sets.
+    intros x1 H'1 H'2; try exact H'2.
+    generalize H'1.
+    elim H'2; auto with sets.
+  Qed.
+  
+  Theorem Union_add :
+    forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
+  Proof.
+    unfold Add in |- *; auto using Union_associative with sets.
+  Qed.
+  
+  Theorem Non_disjoint_union :
+    forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
+  Proof.
+    intros X x H'; unfold Add in |- *.
+    apply Extensionality_Ensembles; red in |- *.
+    split; red in |- *; auto with sets.
+    intros x0 H'0; elim H'0; auto with sets.
+    intros t H'1; elim H'1; auto with sets.
+  Qed.
+  
+  Theorem Non_disjoint_union' :
+    forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
+  Proof.
+    intros X x H'; unfold Subtract in |- *.
+    apply Extensionality_Ensembles.
+    split; red in |- *; auto with sets.
+    intros x0 H'0; elim H'0; auto with sets.
+    intros x0 H'0; apply Setminus_intro; auto with sets.
+    red in |- *; intro H'1; elim H'1.
+    lapply (Singleton_inv U x x0); auto with sets.
+    intro H'4; apply H'; rewrite H'4; auto with sets.
+  Qed.
+  
+  Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
+  Proof.
+    intro x; rewrite (Empty_set_zero' x); auto with sets.
+  Qed.
+  
+  Lemma incl_add :
+    forall (A B:Ensemble U) (x:U),
+      Included U A B -> Included U (Add U A x) (Add U B x).
+  Proof.
+    intros A B x H'; red in |- *; auto with sets.
+    intros x0 H'0.
+    lapply (Add_inv U A x x0); auto with sets.
+    intro H'1; elim H'1;
+      [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
+      auto with sets.
+  Qed.
 
-Lemma less_than_empty :
- forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
-Proof.
-auto with sets.
-Qed.
-Hint Resolve less_than_empty.
+  Lemma incl_add_x :
+    forall (A B:Ensemble U) (x:U),
+      ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
+  Proof.
+    unfold Included in |- *.
+    intros A B x H' H'0 x0 H'1.
+    lapply (H'0 x0); auto with sets.
+    intro H'2; lapply (Add_inv U B x x0); auto with sets.
+    intro H'3; elim H'3;
+      [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
+    absurd (In U A x0); auto with sets.
+    rewrite <- H'4; auto with sets.
+  Qed.
+  
+  Lemma Add_commutative :
+    forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
+  Proof.
+    intros A x y.
+    unfold Add in |- *.
+    rewrite (Union_associative A (Singleton U x) (Singleton U y)).
+    rewrite (Union_commutative (Singleton U x) (Singleton U y)).
+    rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
+      auto with sets.
+  Qed.
+  
+  Lemma Add_commutative' :
+    forall (A:Ensemble U) (x y z:U),
+      Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
+  Proof.
+    intros A x y z.
+    rewrite (Add_commutative (Add U A x) y z).
+    rewrite (Add_commutative A x z); auto with sets.
+  Qed.
+  
+  Lemma Add_distributes :
+    forall (A B:Ensemble U) (x y:U),
+      Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
+  Proof.
+    intros A B x y H'; try assumption.
+    rewrite <- (Union_add (Add U A x) B y).
+    unfold Add at 4 in |- *.
+    rewrite (Union_commutative A (Singleton U x)).
+    rewrite Union_associative.
+    rewrite (Union_absorbs A B H').
+    rewrite (Union_commutative (Singleton U x) A).
+    auto with sets.
+  Qed.
 
-Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
-Proof.
-auto with sets.
-Qed.
-
-Theorem Union_associative :
- forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
-Proof.
-auto 9 with sets.
-Qed.
-Hint Resolve Union_associative.
-
-Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
-Proof.
-auto 7 with sets.
-Qed.
-
-Lemma Union_absorbs :
- forall A B:Ensemble U, Included U B A -> Union U A B = A.
-Proof.
-auto 7 with sets.
-Qed.
-
-Theorem Couple_as_union :
- forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
-Proof.
-intros x y; apply Extensionality_Ensembles; split; red in |- *.
-intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
-intros x0 H'; elim H'; auto with sets.
-Qed.
-
-Theorem Triple_as_union :
- forall x y z:U,
-   Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
-   Triple U x y z.
-Proof.
-intros x y z; apply Extensionality_Ensembles; split; red in |- *.
-intros x0 H'; elim H'.
-intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
-intros x1 H'0; elim H'0; auto with sets.
-intros x0 H'; elim H'; auto with sets.
-Qed.
-
-Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
-Proof.
-intros x y.
-rewrite <- (Couple_as_union x y).
-rewrite <- (Union_idempotent (Singleton U x)).
-apply Triple_as_union.
-Qed.
-
-Theorem Triple_as_Couple_Singleton :
- forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
-Proof.
-intros x y z.
-rewrite <- (Triple_as_union x y z).
-rewrite <- (Couple_as_union x y); auto with sets.
-Qed.
-
-Theorem Intersection_commutative :
- forall A B:Ensemble U, Intersection U A B = Intersection U B A.
-Proof.
-intros A B.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x H'; elim H'; auto with sets.
-Qed.
-
-Theorem Distributivity :
- forall A B C:Ensemble U,
-   Intersection U A (Union U B C) =
-   Union U (Intersection U A B) (Intersection U A C).
-Proof.
-intros A B C.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x H'.
-elim H'.
-intros x0 H'0 H'1; generalize H'0.
-elim H'1; auto with sets.
-elim H'; intros x0 H'0; elim H'0; auto with sets.
-Qed.
-
-Theorem Distributivity' :
- forall A B C:Ensemble U,
-   Union U A (Intersection U B C) =
-   Intersection U (Union U A B) (Union U A C).
-Proof.
-intros A B C.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x H'.
-elim H'; auto with sets.
-intros x0 H'0; elim H'0; auto with sets.
-elim H'.
-intros x0 H'0; elim H'0; auto with sets.
-intros x1 H'1 H'2; try exact H'2.
-generalize H'1.
-elim H'2; auto with sets.
-Qed.
-
-Theorem Union_add :
- forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
-Proof.
-unfold Add in |- *; auto with sets.
-Qed.
-Hint Resolve Union_add.
-
-Theorem Non_disjoint_union :
- forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
-intros X x H'; unfold Add in |- *.
-apply Extensionality_Ensembles; red in |- *.
-split; red in |- *; auto with sets.
-intros x0 H'0; elim H'0; auto with sets.
-intros t H'1; elim H'1; auto with sets.
-Qed.
-
-Theorem Non_disjoint_union' :
- forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
-Proof.
-intros X x H'; unfold Subtract in |- *.
-apply Extensionality_Ensembles.
-split; red in |- *; auto with sets.
-intros x0 H'0; elim H'0; auto with sets.
-intros x0 H'0; apply Setminus_intro; auto with sets.
-red in |- *; intro H'1; elim H'1.
-lapply (Singleton_inv U x x0); auto with sets.
-intro H'4; apply H'; rewrite H'4; auto with sets.
-Qed.
-
-Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
-Proof.
-intro x; rewrite (Empty_set_zero' x); auto with sets.
-Qed.
-Hint Resolve singlx.
-
-Lemma incl_add :
- forall (A B:Ensemble U) (x:U),
-   Included U A B -> Included U (Add U A x) (Add U B x).
-Proof.
-intros A B x H'; red in |- *; auto with sets.
-intros x0 H'0.
-lapply (Add_inv U A x x0); auto with sets.
-intro H'1; elim H'1;
- [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
- auto with sets.
-Qed.
-Hint Resolve incl_add.
-
-Lemma incl_add_x :
- forall (A B:Ensemble U) (x:U),
-   ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
-Proof.
-unfold Included in |- *.
-intros A B x H' H'0 x0 H'1.
-lapply (H'0 x0); auto with sets.
-intro H'2; lapply (Add_inv U B x x0); auto with sets.
-intro H'3; elim H'3;
- [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
-absurd (In U A x0); auto with sets.
-rewrite <- H'4; auto with sets.
-Qed.
-
-Lemma Add_commutative :
- forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
-Proof.
-intros A x y.
-unfold Add in |- *.
-rewrite (Union_associative A (Singleton U x) (Singleton U y)).
-rewrite (Union_commutative (Singleton U x) (Singleton U y)).
-rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
- auto with sets.
-Qed.
-
-Lemma Add_commutative' :
- forall (A:Ensemble U) (x y z:U),
-   Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
-Proof.
-intros A x y z.
-rewrite (Add_commutative (Add U A x) y z).
-rewrite (Add_commutative A x z); auto with sets.
-Qed.
-
-Lemma Add_distributes :
- forall (A B:Ensemble U) (x y:U),
-   Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
-Proof.
-intros A B x y H'; try assumption.
-rewrite <- (Union_add (Add U A x) B y).
-unfold Add at 4 in |- *.
-rewrite (Union_commutative A (Singleton U x)).
-rewrite Union_associative.
-rewrite (Union_absorbs A B H').
-rewrite (Union_commutative (Singleton U x) A).
-auto with sets.
-Qed.
-
-Lemma setcover_intro :
- forall (U:Type) (A x y:Ensemble U),
-   Strict_Included U x y ->
-   ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->
-   covers (Ensemble U) (Power_set_PO U A) y x.
-Proof.
-intros; apply Definition_of_covers; auto with sets.
-Qed.
-Hint Resolve setcover_intro.
+  Lemma setcover_intro :
+    forall (U:Type) (A x y:Ensemble U),
+      Strict_Included U x y ->
+      ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->
+      covers (Ensemble U) (Power_set_PO U A) y x.
+  Proof.
+    intros; apply Definition_of_covers; auto with sets.
+  Qed.
 
 End Sets_as_an_algebra.
 
-- 
cgit v1.2.3