modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes

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

19 files changed, 218 insertions, 218 deletions

diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 72c99fc10..8be8c47fa 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -55,7 +55,7 @@ intros n m; pattern n, m in |- *; apply nat_double_ind;
 Qed.
 
 Lemma even_odd_cor :
- forall n:nat,  exists p : nat | n = (2 * p)%nat \/ n = S (2 * p).
+ forall n:nat,  exists p : nat, n = (2 * p)%nat \/ n = S (2 * p).
 intro.
 assert (H := even_or_odd n).
 exists (div2 n).
@@ -87,7 +87,7 @@ Qed.
 Lemma euclidian_division :
  forall x y:R,
    y <> 0 ->
-    exists k : Z | ( exists r : R | x = IZR k * y + r /\ 0 <= r < Rabs y).
+    exists k : Z, (exists r : R, x = IZR k * y + r /\ 0 <= r < Rabs y).
 intros.
 pose
  (k0 :=
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 5eab01e5b..d7531e49f 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -20,9 +20,9 @@ Theorem MVT :
    a < b ->
    (forall c:R, a <= c <= b -> continuity_pt f c) ->
    (forall c:R, a <= c <= b -> continuity_pt g c) ->
-    exists c : R
-   | ( exists P : a < c < b
-      | (g b - g a) * derive_pt f c (pr1 c P) =
+    exists c : R,
+     (exists P : a < c < b,
+        (g b - g a) * derive_pt f c (pr1 c P) =
         (f b - f a) * derive_pt g c (pr2 c P)).
 intros; assert (H2 := Rlt_le _ _ H).
 pose (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y).
@@ -140,7 +140,7 @@ Qed.
 Lemma MVT_cor1 :
  forall (f:R -> R) (a b:R) (pr:derivable f),
    a < b ->
-    exists c : R | f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b.
+    exists c : R, f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b.
 intros f a b pr H; cut (forall c:R, a < c < b -> derivable_pt f c);
  [ intro | intros; apply pr ].
 cut (forall c:R, a < c < b -> derivable_pt id c);
@@ -164,7 +164,7 @@ Theorem MVT_cor2 :
  forall (f f':R -> R) (a b:R),
    a < b ->
    (forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) ->
-    exists c : R | f b - f a = f' c * (b - a) /\ a < c < b.
+    exists c : R, f b - f a = f' c * (b - a) /\ a < c < b.
 intros f f' a b H H0; cut (forall c:R, a <= c <= b -> derivable_pt f c).
 intro; cut (forall c:R, a < c < b -> derivable_pt f c).
 intro; cut (forall c:R, a <= c <= b -> continuity_pt f c).
@@ -194,9 +194,9 @@ Lemma MVT_cor3 :
  forall (f f':R -> R) (a b:R),
    a < b ->
    (forall x:R, a <= x -> x <= b -> derivable_pt_lim f x (f' x)) ->
-    exists c : R | a <= c /\ c <= b /\ f b = f a + f' c * (b - a).
+    exists c : R, a <= c /\ c <= b /\ f b = f a + f' c * (b - a).
 intros f f' a b H H0;
- assert (H1 :  exists c : R | f b - f a = f' c * (b - a) /\ a < c < b);
+ assert (H1 :  exists c : R, f b - f a = f' c * (b - a) /\ a < c < b);
  [ apply MVT_cor2; [ apply H | intros; elim H1; intros; apply (H0 _ H2 H3) ]
  | elim H1; intros; exists x; elim H2; intros; elim H4; intros; split;
     [ left; assumption | split; [ left; assumption | rewrite <- H3; ring ] ] ].
@@ -207,7 +207,7 @@ Lemma Rolle :
    (forall x:R, a <= x <= b -> continuity_pt f x) ->
    a < b ->
    f a = f b ->
-    exists c : R | ( exists P : a < c < b | derive_pt f c (pr c P) = 0).
+    exists c : R, (exists P : a < c < b, derive_pt f c (pr c P) = 0).
 intros; assert (H2 : forall x:R, a < x < b -> derivable_pt id x).
 intros; apply derivable_pt_id.
 assert (H3 := MVT f id a b pr H2 H0 H);
@@ -669,7 +669,7 @@ Lemma antiderivative_Ucte :
  forall (f g1 g2:R -> R) (a b:R),
    antiderivative f g1 a b ->
    antiderivative f g2 a b ->
-    exists c : R | (forall x:R, a <= x <= b -> g1 x = g2 x + c).
+    exists c : R, (forall x:R, a <= x <= b -> g1 x = g2 x + c).
 unfold antiderivative in |- *; intros; elim H; clear H; intros; elim H0;
  clear H0; intros H0 _; exists (g1 a - g2 a); intros;
  assert (H3 : forall x:R, a <= x <= b -> derivable_pt g1 x).
@@ -696,4 +696,4 @@ apply derivable_pt_lim_minus; [ elim (H _ H9) | elim (H0 _ H9) ]; intros;
 assert (H8 := null_derivative_loc (g1 - g2)%F a b H5 H6 H7);
  unfold constant_D_eq in H8; assert (H9 := H8 _ H2); 
  unfold minus_fct in H9; rewrite <- H9; ring.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 4111377b7..b6375829b 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -22,8 +22,8 @@ Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R)
   (r:posreal) : Prop :=
   forall eps:R,
     0 < eps ->
-     exists N : nat
-    | (forall (n:nat) (y:R),
+     exists N : nat,
+      (forall (n:nat) (y:R),
          (N <= n)%nat -> Boule x r y -> Rabs (f y - fn n y) < eps). 
 
 (* Normal convergence *)
@@ -104,7 +104,7 @@ cut (0 < eps / 3);
     [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
 elim (H _ H3); intros N0 H4.
 assert (H5 := H0 N0 y H1).
-cut ( exists del : posreal | (forall h:R, Rabs h < del -> Boule x r (y + h))).
+cut (exists del : posreal, (forall h:R, Rabs h < del -> Boule x r (y + h))).
 intro.
 elim H6; intros del1 H7.
 unfold continuity_pt in H5; unfold continue_in in H5; unfold limit1_in in H5;
@@ -256,4 +256,4 @@ unfold An in |- *; apply H4; unfold Boule in |- *; simpl in |- *;
  rewrite Rminus_0_r; pattern (Rabs x) at 1 in |- *; 
  rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1.
 apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index ad67223ad..346938735 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1306,7 +1306,7 @@ Hint Resolve not_1_INR: real.
 
 
 (**********)
-Lemma IZN : forall n:Z, (0 <= n)%Z ->  exists m : nat | n = Z_of_nat m.
+Lemma IZN : forall n:Z, (0 <= n)%Z ->  exists m : nat, n = Z_of_nat m.
 intros z; idtac; apply Z_of_nat_complete; assumption.
 Qed.
 
@@ -1483,7 +1483,7 @@ Lemma tech_single_z_r_R1 :
  forall r (n:Z),
    r < IZR n ->
    IZR n <= r + 1 ->
-   ( exists s : Z | s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False.
+   (exists s : Z, s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False.
 intros r z H1 H2 [s [H3 [H4 H5]]].
 apply H3; apply single_z_r_R1 with r; trivial.
 Qed.
@@ -1626,6 +1626,6 @@ Qed.
 (**********)
 Lemma completeness_weak :
  forall E:R -> Prop,
-   bound E -> ( exists x : R | E x) ->  exists m : R | is_lub E m.
+   bound E -> (exists x : R, E x) ->  exists m : R, is_lub E m.
 intros; elim (completeness E H H0); intros; split with x; assumption.
 Qed.
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 40848009a..6a2d3bdd7 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -120,7 +120,7 @@ Qed.
 
 Lemma AbsList_P2 :
  forall (l:Rlist) (x y:R),
-   In y (AbsList l x) ->  exists z : R | In z l /\ y = Rabs (z - x) / 2.
+   In y (AbsList l x) ->  exists z : R, In z l /\ y = Rabs (z - x) / 2.
 intros; induction  l as [| r l Hrecl].
 elim H.
 elim H; intro.
@@ -132,7 +132,7 @@ assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros;
 Qed.
 
 Lemma MaxRlist_P2 :
- forall l:Rlist, ( exists y : R | In y l) -> In (MaxRlist l) l.
+ forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l.
 intros; induction  l as [| r l Hrecl].
 simpl in H; elim H; trivial.
 induction  l as [| r0 l Hrecl0].
@@ -164,7 +164,7 @@ Qed.
 
 Lemma pos_Rl_P2 :
  forall (l:Rlist) (x:R),
-   In x l <-> ( exists i : nat | (i < Rlength l)%nat /\ x = pos_Rl l i).
+   In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i).
 intros; induction  l as [| r l Hrecl].
 split; intro;
  [ elim H | elim H; intros; elim H0; intros; elim (lt_n_O _ H1) ].
@@ -186,9 +186,9 @@ Qed.
 
 Lemma Rlist_P1 :
  forall (l:Rlist) (P:R -> R -> Prop),
-   (forall x:R, In x l ->  exists y : R | P x y) ->
-    exists l' : Rlist
-   | Rlength l = Rlength l' /\
+   (forall x:R, In x l ->  exists y : R, P x y) ->
+    exists l' : Rlist,
+     Rlength l = Rlength l' /\
      (forall i:nat, (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i)).
 intros; induction  l as [| r l Hrecl].
 exists nil; intros; split;
@@ -196,7 +196,7 @@ exists nil; intros; split;
 assert (H0 : In r (cons r l)).
 simpl in |- *; left; reflexivity.
 assert (H1 := H _ H0);
- assert (H2 : forall x:R, In x l ->  exists y : R | P x y).
+ assert (H2 : forall x:R, In x l ->  exists y : R, P x y).
 intros; apply H; simpl in |- *; right; assumption.
 assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0);
  intros; elim H5; clear H5; intros; split.
@@ -308,7 +308,7 @@ Qed.
 
 Lemma RList_P3 :
  forall (l:Rlist) (x:R),
-   In x l <-> ( exists i : nat | x = pos_Rl l i /\ (i < Rlength l)%nat).
+   In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat).
 intros; split; intro;
  [ induction  l as [| r l Hrecl] | induction  l as [| r l Hrecl] ].
 elim H.
@@ -605,7 +605,7 @@ Qed.
 
 Lemma RList_P19 :
  forall l:Rlist,
-   l <> nil ->  exists r : R | ( exists r0 : Rlist | l = cons r r0).
+   l <> nil ->  exists r : R, (exists r0 : Rlist, l = cons r r0).
 intros; induction  l as [| r l Hrecl];
  [ elim H; reflexivity | exists r; exists l; reflexivity ].
 Qed.
@@ -613,8 +613,8 @@ Qed.
 Lemma RList_P20 :
  forall l:Rlist,
    (2 <= Rlength l)%nat ->
-    exists r : R
-   | ( exists r1 : R | ( exists l' : Rlist | l = cons r (cons r1 l'))). 
+    exists r : R,
+     (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))). 
 intros; induction  l as [| r l Hrecl];
  [ simpl in H; elim (le_Sn_O _ H)
  | induction  l as [| r0 l Hrecl0];
@@ -741,4 +741,4 @@ change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *;
  apply minus_Sn_m; assumption.
 replace (cons r r0) with (cons_Rlist (cons r nil) r0);
  [ symmetry  in |- *; apply RList_P27 | reflexivity ].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 37d987855..492b2571c 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -140,7 +140,7 @@ repeat rewrite <- INR_IZR_INZ; auto with real.
 Qed.
 
 (**********)
-Lemma fp_nat : forall r:R, frac_part r = 0 ->  exists c : Z | r = IZR c.
+Lemma fp_nat : forall r:R, frac_part r = 0 ->  exists c : Z, r = IZR c.
 unfold frac_part in |- *; intros; split with (Int_part r);
  apply Rminus_diag_uniq; auto with zarith real.
 Qed.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index f60c609a0..b7d490225 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -234,8 +234,8 @@ Qed.
 Definition derivable_pt_lim f (x l:R) : Prop :=
   forall eps:R,
     0 < eps ->
-     exists delta : posreal
-    | (forall h:R,
+     exists delta : posreal,
+      (forall h:R,
          h <> 0 -> Rabs h < delta -> Rabs ((f (x + h) - f x) / h - l) < eps).
 
 Definition derivable_pt_abs f (x l:R) : Prop := derivable_pt_lim f x l.
@@ -255,7 +255,7 @@ Arguments Scope derive [Rfun_scope _].
 
 Definition antiderivative f (g:R -> R) (a b:R) : Prop :=
   (forall x:R,
-     a <= x <= b ->  exists pr : derivable_pt g x | f x = derive_pt g x pr) /\
+     a <= x <= b ->  exists pr : derivable_pt g x, f x = derive_pt g x pr) /\
   a <= b.
 (************************************)
 (** Class of differential functions *)
@@ -446,7 +446,7 @@ Qed.
 (***********************************)
 (**********)
 Lemma derivable_derive :
- forall f (x:R) (pr:derivable_pt f x),  exists l : R | derive_pt f x pr = l.
+ forall f (x:R) (pr:derivable_pt f x),  exists l : R, derive_pt f x pr = l.
 intros; exists (projT1 pr).
 unfold derive_pt in |- *; reflexivity.
 Qed.
@@ -1476,4 +1476,4 @@ unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse;
 apply Rplus_lt_reg_r with l.
 unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r; assumption.
 apply Rinv_0_lt_compat; prove_sup0.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index a02c5da6c..980bb2b51 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -395,7 +395,7 @@ Lemma continuous_neq_0 :
  forall (f:R -> R) (x0:R),
    continuity_pt f x0 ->
    f x0 <> 0 ->
-    exists eps : posreal | (forall h:R, Rabs h < eps -> f (x0 + h) <> 0).
+    exists eps : posreal, (forall h:R, Rabs h < eps -> f (x0 + h) <> 0).
 intros; unfold continuity_pt in H; unfold continue_in in H;
  unfold limit1_in in H; unfold limit_in in H; elim (H (Rabs (f x0 / 2))).
 intros; elim H1; intros.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index a047c78c0..62de585bc 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -144,7 +144,7 @@ Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
 Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.
 
 (**********)
-Definition bound (E:R -> Prop) :=  exists m : R | is_upper_bound E m.
+Definition bound (E:R -> Prop) :=  exists m : R, is_upper_bound E m.
 
 (**********)
 Definition is_lub (E:R -> Prop) (m:R) :=
@@ -154,4 +154,4 @@ Definition is_lub (E:R -> Prop) (m:R) :=
 Axiom
   completeness :
     forall E:R -> Prop,
-      bound E -> ( exists x : R | E x) -> sigT (fun m:R => is_lub E m).
+      bound E -> (exists x : R, E x) -> sigT (fun m:R => is_lub E m).
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 62eff1d1f..188699e6d 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -226,10 +226,10 @@ Lemma Pow_x_infinity :
  forall x:R,
    Rabs x > 1 ->
    forall b:R,
-      exists N : nat | (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b).
+      exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b).
 Proof.
 intros; elim (archimed (b * / (Rabs x - 1))); intros; clear H1;
- cut ( exists N : nat | INR N >= b * / (Rabs x - 1)).
+ cut (exists N : nat, INR N >= b * / (Rabs x - 1)).
 intro; elim H1; clear H1; intros; exists x0; intros;
  apply (Rge_trans (Rabs (x ^ n)) (Rabs (x ^ x0)) b).
 apply Rle_ge; apply Power_monotonic; assumption.
@@ -289,7 +289,7 @@ Lemma pow_lt_1_zero :
    Rabs x < 1 ->
    forall y:R,
      0 < y ->
-      exists N : nat | (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y).
+      exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y).
 Proof.
 intros; elim (Req_dec x 0); intro. 
 exists 1%nat; rewrite H1; intros n GE; rewrite pow_ne_zero.
@@ -789,5 +789,5 @@ Qed.
 Definition infinit_sum (s:nat -> R) (l:R) : Prop :=
   forall eps:R,
     eps > 0 ->
-     exists N : nat
-    | (forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps).
\ No newline at end of file
+     exists N : nat,
+      (forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps).
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 2766aa2fe..8b087856c 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -427,7 +427,7 @@ Lemma maxN :
    a < b ->
    sigT (fun n:nat => a + INR n * del < b /\ b <= a + INR (S n) * del).
 intros; pose (I := fun n:nat => a + INR n * del < b);
- assert (H0 :  exists n : nat | I n).
+ assert (H0 :  exists n : nat, I n).
 exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r;
  assumption.
 cut (Nbound I).
@@ -498,7 +498,7 @@ intro f; intros;
 unfold bound in |- *; exists (b - a); unfold is_upper_bound in |- *; intros;
  unfold E in H1; elim H1; clear H1; intros H1 _; elim H1; 
  intros; assumption.
-assert (H2 :  exists x : R | E x).
+assert (H2 :  exists x : R, E x).
 assert (H2 := Heine f (fun x:R => a <= x <= b) (compact_P3 a b) H0 eps);
  elim H2; intros; exists (Rmin x (b - a)); unfold E in |- *; 
  split;
@@ -512,7 +512,7 @@ assert (H3 := completeness E H1 H2); elim H3; intros; cut (0 < x <= b - a).
 intro; elim H4; clear H4; intros; apply existT with (mkposreal _ H4); split.
 apply H5.
 unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6;
- pose (D := Rabs (x0 - y)); elim (classic ( exists y : R | D < y /\ E y));
+ pose (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y));
  intro.
 elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13;
  intros; apply H15; assumption.
@@ -701,8 +701,8 @@ intros; rewrite H2 in H7; rewrite H3 in H7; simpl in |- *;
   (forall t:R,
      a <= t <= b ->
      t = b \/
-     ( exists i : nat
-      | (i < pred (Rlength (SubEqui del H)))%nat /\
+     (exists i : nat,
+        (i < pred (Rlength (SubEqui del H)))%nat /\
         co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i))
           t)).
 intro; elim (H8 _ H7); intro.
@@ -744,7 +744,7 @@ apply Rge_minus; apply Rle_ge; assumption.
 intros; clear H0 H1 H4 phi H5 H6 t H7; case (Req_dec t0 b); intro.
 left; assumption.
 right; pose (I := fun j:nat => a + INR j * del <= t0);
- assert (H1 :  exists n : nat | I n).
+ assert (H1 :  exists n : nat, I n).
 exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r; elim H8;
  intros; assumption.
 assert (H4 : Nbound I).
@@ -818,15 +818,15 @@ unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv);
 unfold RiemannInt in |- *; case (RiemannInt_exists pr2 RinvN RinvN_cv);
  intros;
  cut
-  ( exists psi1 : nat -> StepFun a b
-   | (forall n:nat,
+  (exists psi1 : nat -> StepFun a b,
+     (forall n:nat,
         (forall t:R,
            Rmin a b <= t /\ t <= Rmax a b ->
            Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\
         Rabs (RiemannInt_SF (psi1 n)) < RinvN n)).
 cut
- ( exists psi2 : nat -> StepFun b a
-  | (forall n:nat,
+ (exists psi2 : nat -> StepFun b a,
+    (forall n:nat,
        (forall t:R,
           Rmin a b <= t /\ t <= Rmax a b ->
           Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\
@@ -1324,8 +1324,8 @@ replace eps with (3 * (eps / 5) + eps / 5 + eps / 5).
 repeat apply Rplus_lt_compat.
 assert
  (H7 :
-   exists psi1 : nat -> StepFun a b
-  | (forall n:nat,
+   exists psi1 : nat -> StepFun a b,
+    (forall n:nat,
        (forall t:R,
           Rmin a b <= t /\ t <= Rmax a b ->
           Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\
@@ -1334,8 +1334,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
  apply (projT2 (phi_sequence_prop RinvN pr1 n0)).
 assert
  (H8 :
-   exists psi2 : nat -> StepFun a b
-  | (forall n:nat,
+   exists psi2 : nat -> StepFun a b,
+    (forall n:nat,
        (forall t:R,
           Rmin a b <= t /\ t <= Rmax a b ->
           Rabs (g t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\
@@ -1344,8 +1344,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
  apply (projT2 (phi_sequence_prop RinvN pr2 n0)).
 assert
  (H9 :
-   exists psi3 : nat -> StepFun a b
-  | (forall n:nat,
+   exists psi3 : nat -> StepFun a b,
+    (forall n:nat,
        (forall t:R,
           Rmin a b <= t /\ t <= Rmax a b ->
           Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\
@@ -1513,8 +1513,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr N);
  pose (f := fct_cte c);
  assert
   (H1 :
-    exists psi1 : nat -> StepFun a b
-   | (forall n:nat,
+    exists psi1 : nat -> StepFun a b,
+     (forall n:nat,
         (forall t:R,
            Rmin a b <= t /\ t <= Rmax a b ->
            Rabs (f t - phi_sequence RinvN pr n t) <= psi1 n t) /\
@@ -1606,8 +1606,8 @@ apply Rcontinuity_abs.
 pose (phi3 := phi_sequence RinvN pr2);
  assert
   (H0 :
-    exists psi3 : nat -> StepFun a b
-   | (forall n:nat,
+    exists psi3 : nat -> StepFun a b,
+     (forall n:nat,
         (forall t:R,
            Rmin a b <= t /\ t <= Rmax a b ->
            Rabs (Rabs (f t) - phi3 n t) <= psi3 n t) /\
@@ -1616,16 +1616,16 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
  apply (projT2 (phi_sequence_prop RinvN pr2 n)). 
 assert
  (H1 :
-   exists psi2 : nat -> StepFun a b
-  | (forall n:nat,
+   exists psi2 : nat -> StepFun a b,
+    (forall n:nat,
        (forall t:R,
           Rmin a b <= t /\ t <= Rmax a b ->
           Rabs (Rabs (f t) - phi2 n t) <= psi2 n t) /\
        Rabs (RiemannInt_SF (psi2 n)) < RinvN n)).
 assert
  (H1 :
-   exists psi2 : nat -> StepFun a b
-  | (forall n:nat,
+   exists psi2 : nat -> StepFun a b,
+    (forall n:nat,
        (forall t:R,
           Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi2 n t) /\
        Rabs (RiemannInt_SF (psi2 n)) < RinvN n)).
@@ -1656,8 +1656,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr1 N);
  change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) x) in |- *;
  assert
   (H1 :
-    exists psi1 : nat -> StepFun a b
-   | (forall n:nat,
+    exists psi1 : nat -> StepFun a b,
+     (forall n:nat,
         (forall t:R,
            Rmin a b <= t /\ t <= Rmax a b ->
            Rabs (f t - phi1 n t) <= psi1 n t) /\
@@ -1681,8 +1681,8 @@ cut (forall N:nat, IsStepFun (phi2_aux N) a b).
 intro; pose (phi2_m := fun N:nat => mkStepFun (X N)).
 assert
  (H2 :
-   exists psi2 : nat -> StepFun a b
-  | (forall n:nat,
+   exists psi2 : nat -> StepFun a b,
+    (forall n:nat,
        (forall t:R,
           Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi2 n t) <= psi2 n t) /\
        Rabs (RiemannInt_SF (psi2 n)) < RinvN n)).
@@ -2328,8 +2328,8 @@ apply Rmult_eq_reg_l with 3;
 clear x u x0 x1 eps H H0 N1 H1 N2 H2;
  assert
   (H1 :
-    exists psi1 : nat -> StepFun a b
-   | (forall n:nat,
+    exists psi1 : nat -> StepFun a b,
+     (forall n:nat,
         (forall t:R,
            Rmin a b <= t /\ t <= Rmax a b ->
            Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\
@@ -2338,8 +2338,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
  apply (projT2 (phi_sequence_prop RinvN pr1 n)). 
 assert
  (H2 :
-   exists psi2 : nat -> StepFun b c
-  | (forall n:nat,
+   exists psi2 : nat -> StepFun b c,
+    (forall n:nat,
        (forall t:R,
           Rmin b c <= t /\ t <= Rmax b c ->
           Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\
@@ -2348,8 +2348,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
  apply (projT2 (phi_sequence_prop RinvN pr2 n)). 
 assert
  (H3 :
-   exists psi3 : nat -> StepFun a c
-  | (forall n:nat,
+   exists psi3 : nat -> StepFun a c,
+    (forall n:nat,
        (forall t:R,
           Rmin a c <= t /\ t <= Rmax a c ->
           Rabs (f t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\
@@ -3260,4 +3260,4 @@ intro f; intros; case (Rle_dec a b); intro;
     [ auto with real
     | assert (H0 := RiemannInt_P1 pr); rewrite (RiemannInt_P8 pr H0);
        rewrite (RiemannInt_P33 _ H0 H); ring ] ].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 5f47466ac..19782f2bc 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -21,7 +21,7 @@ Set Implicit Arguments.
 (**************************************************)
 
 Definition Nbound (I:nat -> Prop) : Prop :=
-   exists n : nat | (forall i:nat, I i -> (i <= n)%nat).
+   exists n : nat, (forall i:nat, I i -> (i <= n)%nat).
 
 Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z_of_nat n}.
 intros; apply Z_of_nat_complete_inf; assumption.
@@ -29,15 +29,15 @@ Qed.
 
 Lemma Nzorn :
  forall I:nat -> Prop,
-   ( exists n : nat | I n) ->
+   (exists n : nat, I n) ->
    Nbound I -> sigT (fun n:nat => I n /\ (forall i:nat, I i -> (i <= n)%nat)).
-intros I H H0; pose (E := fun x:R =>  exists i : nat | I i /\ INR i = x);
+intros I H H0; pose (E := fun x:R =>  exists i : nat, I i /\ INR i = x);
  assert (H1 : bound E).
 unfold Nbound in H0; elim H0; intros N H1; unfold bound in |- *;
  exists (INR N); unfold is_upper_bound in |- *; intros; 
  unfold E in H2; elim H2; intros; elim H3; intros; 
  rewrite <- H5; apply le_INR; apply H1; assumption.
-assert (H2 :  exists x : R | E x).
+assert (H2 :  exists x : R, E x).
 elim H; intros; exists (INR x); unfold E in |- *; exists x; split;
  [ assumption | reflexivity ].
 assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p;
@@ -311,8 +311,8 @@ Lemma StepFun_P10 :
  forall (f:R -> R) (l lf:Rlist) (a b:R),
    a <= b ->
    adapted_couple f a b l lf ->
-    exists l' : Rlist
-   | ( exists lf' : Rlist | adapted_couple_opt f a b l' lf').
+    exists l' : Rlist,
+     (exists lf' : Rlist, adapted_couple_opt f a b l' lf').
 simple induction l.
 intros; unfold adapted_couple in H0; decompose [and] H0; simpl in H4;
  discriminate.
@@ -886,8 +886,8 @@ Qed.
 Lemma StepFun_P16 :
  forall (f:R -> R) (l lf:Rlist) (a b:R),
    adapted_couple f a b l lf ->
-    exists l' : Rlist
-   | ( exists lf' : Rlist | adapted_couple_opt f a b l' lf'). 
+    exists l' : Rlist,
+     (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). 
 intros; case (Rle_dec a b); intro;
  [ apply (StepFun_P10 r H)
  | assert (H1 : b <= a);
@@ -1086,14 +1086,14 @@ apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl in |- *;
  apply lt_O_Sn.
 intros; unfold constant_D_eq, open_interval in |- *; intros;
  cut
-  ( exists l : R
-   | constant_D_eq f
+  (exists l : R,
+     constant_D_eq f
        (open_interval (pos_Rl (cons_ORlist lf lg) i)
           (pos_Rl (cons_ORlist lf lg) (S i))) l).
 intros; elim H11; clear H11; intros; assert (H12 := H11);
  assert
   (Hyp_cons :
-    exists r : R | ( exists r0 : Rlist | cons_ORlist lf lg = cons r r0)).
+    exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)).
 apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8).
 elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons;
  unfold FF in |- *; rewrite RList_P12.
@@ -1155,7 +1155,7 @@ pose
  assert (H12 : Nbound I).
 unfold Nbound in |- *; exists (Rlength lf); intros; unfold I in H12; elim H12;
  intros; apply lt_le_weak; assumption.
-assert (H13 :  exists n : nat | I n).
+assert (H13 :  exists n : nat, I n).
 exists 0%nat; unfold I in |- *; split.
 apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0).
 right; symmetry  in |- *.
@@ -1335,14 +1335,14 @@ apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl in |- *;
  apply lt_O_Sn.
 unfold constant_D_eq, open_interval in |- *; intros;
  cut
-  ( exists l : R
-   | constant_D_eq g
+  (exists l : R,
+     constant_D_eq g
        (open_interval (pos_Rl (cons_ORlist lf lg) i)
           (pos_Rl (cons_ORlist lf lg) (S i))) l).
 intros; elim H11; clear H11; intros; assert (H12 := H11);
  assert
   (Hyp_cons :
-    exists r : R | ( exists r0 : Rlist | cons_ORlist lf lg = cons r r0)).
+    exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)).
 apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8).
 elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons;
  unfold FF in |- *; rewrite RList_P12.
@@ -1402,7 +1402,7 @@ pose
  assert (H12 : Nbound I).
 unfold Nbound in |- *; exists (Rlength lg); intros; unfold I in H12; elim H12;
  intros; apply lt_le_weak; assumption.
-assert (H13 :  exists n : nat | I n).
+assert (H13 :  exists n : nat, I n).
 exists 0%nat; unfold I in |- *; split.
 apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0).
 right; symmetry  in |- *; rewrite H1; rewrite <- H6; apply RList_P15;
@@ -2629,4 +2629,4 @@ apply StepFun_P6; assumption.
 split; [ assumption | auto with real ].
 apply StepFun_P6; apply StepFun_P41 with b;
  auto with real || apply StepFun_P6; assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 5fb50822b..e6a2f70a7 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -156,8 +156,8 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X')
   (D:Base X -> Prop) (x0:Base X) (l:Base X') :=
   forall eps:R,
     eps > 0 ->
-     exists alp : R
-    | alp > 0 /\
+     exists alp : R,
+      alp > 0 /\
       (forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps). 
 
 (*******************************)
@@ -323,7 +323,7 @@ Qed.
 
 (*********)
 Definition adhDa (D:R -> Prop) (a:R) : Prop :=
-  forall alp:R, alp > 0 ->  exists x : R | D x /\ R_dist x a < alp.
+  forall alp:R, alp > 0 ->  exists x : R, D x /\ R_dist x a < alp.
 
 (*********)
 Lemma single_limit :
@@ -554,4 +554,4 @@ change (0 < Rabs l / 2) in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat;
     [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *;
        intro; assumption
     | discriminate ] ].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 03544af4b..d8be38f65 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -35,27 +35,27 @@ Fixpoint Rmax_N (N:nat) : R :=
   end.
 
 (*********)
-Definition EUn r : Prop :=  exists i : nat | r = Un i.
+Definition EUn r : Prop :=  exists i : nat, r = Un i.
 
 (*********)
 Definition Un_cv (l:R) : Prop :=
   forall eps:R,
     eps > 0 ->
-     exists N : nat | (forall n:nat, (n >= N)%nat -> R_dist (Un n) l < eps).
+     exists N : nat, (forall n:nat, (n >= N)%nat -> R_dist (Un n) l < eps).
 
 (*********)
 Definition Cauchy_crit : Prop :=
   forall eps:R,
     eps > 0 ->
-     exists N : nat
-    | (forall n m:nat,
+     exists N : nat,
+      (forall n m:nat,
          (n >= N)%nat -> (m >= N)%nat -> R_dist (Un n) (Un m) < eps).
 
 (*********)
 Definition Un_growing : Prop := forall n:nat, Un n <= Un (S n).
 
 (*********)
-Lemma EUn_noempty :  exists r : R | EUn r.
+Lemma EUn_noempty :  exists r : R, EUn r.
 unfold EUn in |- *; split with (Un 0); split with 0%nat; trivial.
 Qed.
 
@@ -99,7 +99,7 @@ Qed.
 
 (* classical is needed: [not_all_not_ex] *)
 (*********)
-Lemma Un_cv_crit : Un_growing -> bound EUn ->  exists l : R | Un_cv l.
+Lemma Un_cv_crit : Un_growing -> bound EUn ->  exists l : R, Un_cv l.
 unfold Un_growing, Un_cv in |- *; intros;
  generalize (completeness_weak EUn H0 EUn_noempty); 
  intro; elim H1; clear H1; intros; split with x; intros; 
@@ -107,7 +107,7 @@ unfold Un_growing, Un_cv in |- *; intros;
  elim H0; clear H0; intros; elim H1; clear H1; intros; 
  generalize (H3 x0 H0); intro; cut (forall n:nat, Un n <= x); 
  intro.
-cut ( exists N : nat | x - eps < Un N).
+cut (exists N : nat, x - eps < Un N).
 intro; elim H6; clear H6; intros; split with x1.
 intros; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps).
 unfold Rgt in H2;
@@ -140,7 +140,7 @@ Qed.
 
 (*********)
 Lemma finite_greater :
- forall N:nat,  exists M : R | (forall n:nat, (n <= N)%nat -> Un n <= M).
+ forall N:nat,  exists M : R, (forall n:nat, (n <= N)%nat -> Un n <= M).
 intro; induction  N as [| N HrecN].
 split with (Un 0); intros; rewrite (le_n_O_eq n H);
  apply (Req_le (Un n) (Un n) (refl_equal (Un n))).
@@ -272,4 +272,4 @@ assumption.
 apply Rabs_pos_lt.
 apply Rinv_neq_0_compat.
 assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 17b884d45..75385b424 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -18,7 +18,7 @@ Require Import Classical_Pred_Type. Open Local Scope R_scope.
 Definition included (D1 D2:R -> Prop) : Prop := forall x:R, D1 x -> D2 x.
 Definition disc (x:R) (delta:posreal) (y:R) : Prop := Rabs (y - x) < delta.
 Definition neighbourhood (V:R -> Prop) (x:R) : Prop :=
-   exists delta : posreal | included (disc x delta) V.
+   exists delta : posreal, included (disc x delta) V.
 Definition open_set (D:R -> Prop) : Prop :=
   forall x:R, D x -> neighbourhood D x.
 Definition complementary (D:R -> Prop) (c:R) : Prop := ~ D c.
@@ -41,7 +41,7 @@ Qed.
 
 Definition point_adherent (D:R -> Prop) (x:R) : Prop :=
   forall V:R -> Prop,
-    neighbourhood V x ->  exists y : R | intersection_domain V D y.
+    neighbourhood V x ->  exists y : R, intersection_domain V D y.
 Definition adherence (D:R -> Prop) (x:R) : Prop := point_adherent D x.
 
 Lemma adherence_P1 : forall D:R -> Prop, included D (adherence D).
@@ -87,7 +87,7 @@ Qed.
 
 Lemma complementary_P1 :
  forall D:R -> Prop,
-   ~ ( exists y : R | intersection_domain D (complementary D) y).
+   ~ (exists y : R, intersection_domain D (complementary D) y).
 intro; red in |- *; intro; elim H; intros;
  unfold intersection_domain, complementary in H0; elim H0; 
  intros; elim H2; assumption.
@@ -111,14 +111,14 @@ intro; unfold closed_set, adherence in |- *;
  pose
   (P :=
    fun V:R -> Prop =>
-     neighbourhood V x ->  exists y : R | intersection_domain V D y);
+     neighbourhood V x ->  exists y : R, intersection_domain V D y);
  assert (H0 := not_all_ex_not _ P H); elim H0; intros V0 H1; 
  unfold P in H1; assert (H2 := imply_to_and _ _ H1);
  unfold neighbourhood in |- *; elim H2; intros; unfold neighbourhood in H3;
  elim H3; intros; exists x0; unfold included in |- *; 
  intros; red in |- *; intro.
 assert (H8 := H7 V0);
- cut ( exists delta : posreal | (forall x:R, disc x1 delta x -> V0 x)).
+ cut (exists delta : posreal, (forall x:R, disc x1 delta x -> V0 x)).
 intro; assert (H10 := H8 H9); elim H4; assumption.
 cut (0 < x0 - Rabs (x - x1)).
 intro; pose (del := mkposreal _ H9); exists del; intros;
@@ -248,8 +248,8 @@ Lemma continuity_P1 :
    continuity_pt f x <->
    (forall W:R -> Prop,
       neighbourhood W (f x) ->
-       exists V : R -> Prop
-      | neighbourhood V x /\ (forall y:R, V y -> W (f y))).
+       exists V : R -> Prop,
+        neighbourhood V x /\ (forall y:R, V y -> W (f y))).
 intros; split.
 intros; unfold neighbourhood in H0.
 elim H0; intros del1 H1.
@@ -329,10 +329,10 @@ Qed.
 Theorem Rsepare :
  forall x y:R,
    x <> y ->
-    exists V : R -> Prop
-   | ( exists W : R -> Prop
-      | neighbourhood V x /\
-        neighbourhood W y /\ ~ ( exists y : R | intersection_domain V W y)).
+    exists V : R -> Prop,
+     (exists W : R -> Prop,
+        neighbourhood V x /\
+        neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)).
 intros x y Hsep; pose (D := Rabs (x - y)).
 cut (0 < D / 2).
 intro; exists (disc x (mkposreal _ H)).
@@ -360,17 +360,17 @@ Qed.
 Record family : Type := mkfamily
   {ind : R -> Prop;
    f :> R -> R -> Prop;
-   cond_fam : forall x:R, ( exists y : R | f x y) -> ind x}.
+   cond_fam : forall x:R, (exists y : R, f x y) -> ind x}.
 
 Definition family_open_set (f:family) : Prop := forall x:R, open_set (f x).
 
 Definition domain_finite (D:R -> Prop) : Prop :=
-   exists l : Rlist | (forall x:R, D x <-> In x l).
+   exists l : Rlist, (forall x:R, D x <-> In x l).
 
 Definition family_finite (f:family) : Prop := domain_finite (ind f).
 
 Definition covering (D:R -> Prop) (f:family) : Prop :=
-  forall x:R, D x ->  exists y : R | f y x.
+  forall x:R, D x ->  exists y : R, f y x.
 
 Definition covering_open_set (D:R -> Prop) (f:family) : Prop :=
   covering D f /\ family_open_set f.
@@ -380,7 +380,7 @@ Definition covering_finite (D:R -> Prop) (f:family) : Prop :=
 
 Lemma restriction_family :
  forall (f:family) (D:R -> Prop) (x:R),
-   ( exists y : R | (fun z1 z2:R => f z1 z2 /\ D z1) x y) ->
+   (exists y : R, (fun z1 z2:R => f z1 z2 /\ D z1) x y) ->
    intersection_domain (ind f) D x.
 intros; elim H; intros; unfold intersection_domain in |- *; elim H0; intros;
  split.
@@ -395,7 +395,7 @@ Definition subfamily (f:family) (D:R -> Prop) : family :=
 Definition compact (X:R -> Prop) : Prop :=
   forall f:family,
     covering_open_set X f ->
-     exists D : R -> Prop | covering_finite X (subfamily f D).
+     exists D : R -> Prop, covering_finite X (subfamily f D).
 
 (**********)
 Lemma family_P1 :
@@ -418,7 +418,7 @@ unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3;
 Qed.
 
 Definition bounded (D:R -> Prop) : Prop :=
-   exists m : R | ( exists M : R | (forall x:R, D x -> m <= x <= M)).
+   exists m : R, (exists M : R, (forall x:R, D x -> m <= x <= M)).
 
 Lemma open_set_P6 :
  forall D1 D2:R -> Prop, open_set D1 -> D1 =_D D2 -> open_set D2.
@@ -433,7 +433,7 @@ Qed.
 Lemma compact_P1 : forall X:R -> Prop, compact X -> bounded X.
 intros; unfold compact in H; pose (D := fun x:R => True);
  pose (g := fun x y:R => Rabs y < x);
- cut (forall x:R, ( exists y : _ | g x y) -> True);
+ cut (forall x:R, (exists y : _, g x y) -> True);
  [ intro | intro; trivial ].
 pose (f0 := mkfamily D g H0); assert (H1 := H f0);
  cut (covering_open_set X f0).
@@ -498,7 +498,7 @@ assumption.
 cut (forall y:R, X y -> 0 < Rabs (y - x) / 2).
 intro; pose (D := X);
  pose (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y);
- cut (forall x:R, ( exists y : _ | g x y) -> D x).
+ cut (forall x:R, (exists y : _, g x y) -> D x).
 intro; pose (f0 := mkfamily D g H3); assert (H4 := H f0);
  cut (covering_open_set X f0).
 intro; assert (H6 := H4 H5); elim H6; clear H6; intros D' H6.
@@ -600,11 +600,11 @@ unfold compact in |- *; intros;
   (A :=
    fun x:R =>
      a <= x <= b /\
-     ( exists D : R -> Prop
-      | covering_finite (fun c:R => a <= c <= x) (subfamily f0 D)));
+     (exists D : R -> Prop,
+        covering_finite (fun c:R => a <= c <= x) (subfamily f0 D)));
  cut (A a).
 intro; cut (bound A).
-intro; cut ( exists a0 : R | A a0).
+intro; cut (exists a0 : R, A a0).
 intro; assert (H3 := completeness A H1 H2); elim H3; clear H3; intros m H3;
  unfold is_lub in H3; cut (a <= m <= b).
 intro; unfold covering_open_set in H; elim H; clear H; intros;
@@ -612,7 +612,7 @@ intro; unfold covering_open_set in H; elim H; clear H; intros;
  clear H6; intros y0 H6; unfold family_open_set in H5; 
  assert (H7 := H5 y0); unfold open_set in H7; assert (H8 := H7 m H6);
  unfold neighbourhood in H8; elim H8; clear H8; intros eps H8;
- cut ( exists x : R | A x /\ m - eps < x <= m).
+ cut (exists x : R, A x /\ m - eps < x <= m).
 intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros;
  case (Req_dec m b); intro.
 rewrite H11 in H10; rewrite H11 in H8; unfold A in H9; elim H9; clear H9;
@@ -751,7 +751,7 @@ unfold intersection_domain in H17.
 split.
 elim H17; intros; assumption.
 unfold Db in |- *; left; elim H17; intros; assumption.
-elim (classic ( exists x : R | A x /\ m - eps < x <= m)); intro.
+elim (classic (exists x : R, A x /\ m - eps < x <= m)); intro.
 assumption.
 elim H3; intros; cut (is_upper_bound A (m - eps)).
 intro; assert (H13 := H11 _ H12); cut (m - eps < m).
@@ -810,12 +810,12 @@ Qed.
 
 Lemma compact_P4 :
  forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F.
-unfold compact in |- *; intros; elim (classic ( exists z : R | F z));
+unfold compact in |- *; intros; elim (classic (exists z : R, F z));
  intro Hyp_F_NE.
 pose (D := ind f0); pose (g := f f0); unfold closed_set in H0.
 pose (g' := fun x y:R => f0 x y \/ complementary F y /\ D x).
 pose (D' := D).
-cut (forall x:R, ( exists y : R | g' x y) -> D' x).
+cut (forall x:R, (exists y : R, g' x y) -> D' x).
 intro; pose (f' := mkfamily D' g' H3); cut (covering_open_set X f').
 intro; elim (H _ H4); intros DX H5; exists DX.
 unfold covering_finite in |- *; unfold covering_finite in H5; elim H5;
@@ -847,7 +847,7 @@ unfold covering in |- *; unfold covering in H2; intros.
 elim (classic (F x)); intro.
 elim (H2 _ H6); intros y0 H7; exists y0; simpl in |- *; unfold g' in |- *;
  left; assumption.
-cut ( exists z : R | D z).
+cut (exists z : R, D z).
 intro; elim H7; clear H7; intros x0 H7; exists x0; simpl in |- *;
  unfold g' in |- *; right.
 split.
@@ -908,7 +908,7 @@ intro; elim H; clear H; intros; apply (compact_P5 _ H H0).
 Qed.
 
 Definition image_dir (f:R -> R) (D:R -> Prop) (x:R) : Prop :=
-   exists y : R | x = f y /\ D y.
+   exists y : R, x = f y /\ D y.
 
 (**********)
 Lemma continuity_compact :
@@ -918,7 +918,7 @@ unfold compact in |- *; intros; unfold covering_open_set in H1.
 elim H1; clear H1; intros.
 pose (D := ind f1).
 pose (g := fun x y:R => image_rec f0 (f1 x) y).
-cut (forall x:R, ( exists y : R | g x y) -> D x).
+cut (forall x:R, (exists y : R, g x y) -> D x).
 intro; pose (f' := mkfamily D g H3).
 cut (covering_open_set X f').
 intro; elim (H0 f' H4); intros D' H5; exists D'.
@@ -958,8 +958,8 @@ Lemma prolongement_C0 :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall c:R, a <= c <= b -> continuity_pt f c) ->
-    exists g : R -> R
-   | continuity g /\ (forall c:R, a <= c <= b -> g c = f c).
+    exists g : R -> R,
+     continuity g /\ (forall c:R, a <= c <= b -> g c = f c).
 intros; elim H; intro.
 pose
  (h :=
@@ -1153,11 +1153,11 @@ Lemma continuity_ab_maj :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall c:R, a <= c <= b -> continuity_pt f c) ->
-    exists Mx : R | (forall c:R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b.
+    exists Mx : R, (forall c:R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b.
 intros;
  cut
-  ( exists g : R -> R
-   | continuity g /\ (forall c:R, a <= c <= b -> g c = f0 c)).
+  (exists g : R -> R,
+     continuity g /\ (forall c:R, a <= c <= b -> g c = f0 c)).
 intro HypProl.
 elim HypProl; intros g Hcont_eq.
 elim Hcont_eq; clear Hcont_eq; intros Hcont Heq.
@@ -1166,7 +1166,7 @@ assert (H2 := continuity_compact g (fun c:R => a <= c <= b) Hcont H1).
 assert (H3 := compact_P2 _ H2).
 assert (H4 := compact_P1 _ H2).
 cut (bound (image_dir g (fun c:R => a <= c <= b))).
-cut ( exists x : R | image_dir g (fun c:R => a <= c <= b) x).
+cut (exists x : R, image_dir g (fun c:R => a <= c <= b) x).
 intros; assert (H7 := completeness _ H6 H5).
 elim H7; clear H7; intros M H7; cut (image_dir g (fun c:R => a <= c <= b) M).
 intro; unfold image_dir in H8; elim H8; clear H8; intros Mxx H8; elim H8;
@@ -1179,8 +1179,8 @@ apply H9.
 elim (classic (image_dir g (fun c:R => a <= c <= b) M)); intro.
 assumption.
 cut
- ( exists eps : posreal
-  | (forall y:R,
+ (exists eps : posreal,
+    (forall y:R,
        ~
        intersection_domain (disc M eps)
          (image_dir g (fun c:R => a <= c <= b)) y)).
@@ -1207,8 +1207,8 @@ apply Rge_minus; apply Rle_ge; apply H12.
 apply H11.
 apply H7; apply H11.
 cut
- ( exists V : R -> Prop
-  | neighbourhood V M /\
+ (exists V : R -> Prop,
+    neighbourhood V M /\
     (forall y:R,
        ~ intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y)).
 intro; elim H9; intros V H10; elim H10; clear H10; intros.
@@ -1225,8 +1225,8 @@ assert
   not_all_ex_not _
     (fun V:R -> Prop =>
        neighbourhood V M ->
-        exists y : R
-       | intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y) H9).
+        exists y : R,
+         intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y) H9).
 elim H10; intros V0 H11; exists V0; assert (H12 := imply_to_and _ _ H11);
  elim H12; clear H12; intros.
 split.
@@ -1253,7 +1253,7 @@ Lemma continuity_ab_min :
  forall (f:R -> R) (a b:R),
    a <= b ->
    (forall c:R, a <= c <= b -> continuity_pt f c) ->
-    exists mx : R | (forall c:R, a <= c <= b -> f mx <= f c) /\ a <= mx <= b.
+    exists mx : R, (forall c:R, a <= c <= b -> f mx <= f c) /\ a <= mx <= b.
 intros.
 cut (forall c:R, a <= c <= b -> continuity_pt (- f0) c).
 intro; assert (H2 := continuity_ab_maj (- f0)%F a b H H1); elim H2;
@@ -1274,18 +1274,18 @@ Qed.
 
 Definition ValAdh (un:nat -> R) (x:R) : Prop :=
   forall (V:R -> Prop) (N:nat),
-    neighbourhood V x ->  exists p : nat | (N <= p)%nat /\ V (un p).
+    neighbourhood V x ->  exists p : nat, (N <= p)%nat /\ V (un p).
 
 Definition intersection_family (f:family) (x:R) : Prop :=
   forall y:R, ind f y -> f y x.
 
 Lemma ValAdh_un_exists :
- forall (un:nat -> R) (D:=fun x:R =>  exists n : nat | x = INR n)
+ forall (un:nat -> R) (D:=fun x:R =>  exists n : nat, x = INR n)
    (f:=
     fun x:R =>
       adherence
-        (fun y:R => ( exists p : nat | y = un p /\ x <= INR p) /\ D x))
-   (x:R), ( exists y : R | f x y) -> D x.
+        (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x))
+   (x:R), (exists y : R, f x y) -> D x.
 intros; elim H; intros; unfold f in H0; unfold adherence in H0;
  unfold point_adherent in H0;
  assert (H1 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0).
@@ -1296,11 +1296,11 @@ elim (H0 _ H1); intros; unfold intersection_domain in H2; elim H2; intros;
 Qed.
 
 Definition ValAdh_un (un:nat -> R) : R -> Prop :=
-  let D := fun x:R =>  exists n : nat | x = INR n in
+  let D := fun x:R =>  exists n : nat, x = INR n in
   let f :=
     fun x:R =>
       adherence
-        (fun y:R => ( exists p : nat | y = un p /\ x <= INR p) /\ D x) in
+        (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x) in
   intersection_family (mkfamily D f (ValAdh_un_exists un)).
 
 Lemma ValAdh_un_prop :
@@ -1322,8 +1322,8 @@ unfold ValAdh in |- *; intros; unfold ValAdh_un in H;
   (H1 :
    adherence
      (fun y0:R =>
-        ( exists p : nat | y0 = un p /\ INR N <= INR p) /\
-        ( exists n : nat | INR N = INR n)) x).
+        (exists p : nat, y0 = un p /\ INR N <= INR p) /\
+        (exists n : nat, INR N = INR n)) x).
 apply H; exists N; reflexivity.
 unfold adherence in H1; unfold point_adherent in H1; assert (H2 := H1 _ H0);
  elim H2; intros; unfold intersection_domain in H3; 
@@ -1348,7 +1348,7 @@ Definition family_closed_set (f:family) : Prop :=
 Definition intersection_vide_in (D:R -> Prop) (f:family) : Prop :=
   forall x:R,
     (ind f x -> included (f x) D) /\
-    ~ ( exists y : R | intersection_family f y).
+    ~ (exists y : R, intersection_family f y).
 
 Definition intersection_vide_finite_in (D:R -> Prop) 
   (f:family) : Prop := intersection_vide_in D f /\ family_finite f.
@@ -1357,15 +1357,15 @@ Definition intersection_vide_finite_in (D:R -> Prop)
 Lemma compact_P6 :
  forall X:R -> Prop,
    compact X ->
-   ( exists z : R | X z) ->
+   (exists z : R, X z) ->
    forall g:family,
      family_closed_set g ->
      intersection_vide_in X g ->
-      exists D : R -> Prop | intersection_vide_finite_in X (subfamily g D).
+      exists D : R -> Prop, intersection_vide_finite_in X (subfamily g D).
 intros X H Hyp g H0 H1.
 pose (D' := ind g).
 pose (f' := fun x y:R => complementary (g x) y /\ D' x).
-assert (H2 : forall x:R, ( exists y : R | f' x y) -> D' x).
+assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x).
 intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption.
 pose (f0 := mkfamily D' f' H2).
 unfold compact in H; assert (H3 : covering_open_set X f0).
@@ -1397,7 +1397,7 @@ intros; unfold included in |- *; intros; unfold intersection_vide_in in H1;
  elim (H1 x); intros; elim H6; intros; apply H7.
 unfold intersection_domain in H5; elim H5; intros; assumption.
 assumption.
-elim (classic ( exists y : R | intersection_domain (ind g) SF y)); intro Hyp'.
+elim (classic (exists y : R, intersection_domain (ind g) SF y)); intro Hyp'.
 red in |- *; intro; elim H5; intros; unfold intersection_family in H6;
  simpl in H6.
 cut (X x0).
@@ -1418,7 +1418,7 @@ apply H11.
 apply H9.
 apply (cond_fam g); exists x0; assumption.
 unfold covering_finite in H4; elim H4; clear H4; intros H4 _;
- cut ( exists z : R | X z).
+ cut (exists z : R, X z).
 intro; elim H5; clear H5; intros; unfold covering in H4; elim (H4 x0 H5);
  intros; simpl in H6; elim Hyp'; exists x1; elim H6; 
  intros; unfold intersection_domain in |- *; split.
@@ -1435,18 +1435,18 @@ Qed.
 
 Theorem Bolzano_Weierstrass :
  forall (un:nat -> R) (X:R -> Prop),
-   compact X -> (forall n:nat, X (un n)) ->  exists l : R | ValAdh un l.
-intros; cut ( exists l : R | ValAdh_un un l).
+   compact X -> (forall n:nat, X (un n)) ->  exists l : R, ValAdh un l.
+intros; cut (exists l : R, ValAdh_un un l).
 intro; elim H1; intros; exists x; elim (ValAdh_un_prop un x); intros;
  apply (H4 H2).
-assert (H1 :  exists z : R | X z).
+assert (H1 :  exists z : R, X z).
 exists (un 0%nat); apply H0.
-pose (D := fun x:R =>  exists n : nat | x = INR n).
+pose (D := fun x:R =>  exists n : nat, x = INR n).
 pose
  (g :=
   fun x:R =>
-    adherence (fun y:R => ( exists p : nat | y = un p /\ x <= INR p) /\ D x)).
-assert (H2 : forall x:R, ( exists y : R | g x y) -> D x).
+    adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)).
+assert (H2 : forall x:R, (exists y : R, g x y) -> D x).
 intros; elim H2; intros; unfold g in H3; unfold adherence in H3;
  unfold point_adherent in H3.
 assert (H4 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0).
@@ -1456,7 +1456,7 @@ elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5;
  assumption.
 pose (f0 := mkfamily D g H2).
 assert (H3 := compact_P6 X H H1 f0).
-elim (classic ( exists l : R | ValAdh_un un l)); intro.
+elim (classic (exists l : R, ValAdh_un un l)); intro.
 assumption.
 cut (family_closed_set f0).
 intro; cut (intersection_vide_in X f0).
@@ -1480,10 +1480,10 @@ elim (H9 r); intros.
 simpl in H12; unfold intersection_domain in H12; cut (In r l).
 intro; elim (H12 H13); intros; assumption.
 unfold r in |- *; apply MaxRlist_P2;
- cut ( exists z : R | intersection_domain (ind f0) SF z).
+ cut (exists z : R, intersection_domain (ind f0) SF z).
 intro; elim H13; intros; elim (H9 x); intros; simpl in H15;
  assert (H17 := H15 H14); exists x; apply H17.
-elim (classic ( exists z : R | intersection_domain (ind f0) SF z)); intro.
+elim (classic (exists z : R, intersection_domain (ind f0) SF z)); intro.
 assumption.
 elim (H8 0); intros _ H14; elim H1; intros;
  assert
@@ -1517,8 +1517,8 @@ Qed.
 
 Definition uniform_continuity (f:R -> R) (X:R -> Prop) : Prop :=
   forall eps:posreal,
-     exists delta : posreal
-    | (forall x y:R,
+     exists delta : posreal,
+      (forall x y:R,
          X x -> X y -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps).
 
 Lemma is_lub_u :
@@ -1529,11 +1529,11 @@ Qed.
 
 Lemma domain_P1 :
  forall X:R -> Prop,
-   ~ ( exists y : R | X y) \/
-   ( exists y : R | X y /\ (forall x:R, X x -> x = y)) \/
-   ( exists x : R | ( exists y : R | X x /\ X y /\ x <> y)).
-intro; elim (classic ( exists y : R | X y)); intro.
-right; elim H; intros; elim (classic ( exists y : R | X y /\ y <> x)); intro.
+   ~ (exists y : R, X y) \/
+   (exists y : R, X y /\ (forall x:R, X x -> x = y)) \/
+   (exists x : R, (exists y : R, X x /\ X y /\ x <> y)).
+intro; elim (classic (exists y : R, X y)); intro.
+right; elim H; intros; elim (classic (exists y : R, X y /\ y <> x)); intro.
 right; elim H1; intros; elim H2; intros; exists x; exists x0; intros.
 split;
  [ assumption
@@ -1564,7 +1564,7 @@ unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1);
 (* X possède au moins deux éléments distincts *)
 assert
  (X_enc :
-   exists m : R | ( exists M : R | (forall x:R, X x -> m <= x <= M) /\ m < M)).
+   exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)).
 assert (H1 := compact_P1 X H0); unfold bounded in H1; elim H1; intros;
  elim H2; intros; exists x; exists x0; split.
 apply H3.
@@ -1587,14 +1587,14 @@ pose
  (g :=
   fun x y:R =>
     X x /\
-    ( exists del : posreal
-     | (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\
+    (exists del : posreal,
+       (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\
        is_lub
          (fun zeta:R =>
             0 < zeta <= M - m /\
             (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2))
          del /\ disc x (mkposreal (del / 2) (H1 del)) y)).
-assert (H2 : forall x:R, ( exists y : R | g x y) -> X x).
+assert (H2 : forall x:R, (exists y : R, g x y) -> X x).
 intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _;
  apply H3.
 pose (f' := mkfamily X g H2); unfold compact in H0;
@@ -1616,7 +1616,7 @@ assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4;
 unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *;
  unfold E in |- *; intros; elim H6; clear H6; intros H6 _; 
  elim H6; clear H6; intros _ H6; apply H6.
-assert (H7 :  exists x : R | E x).
+assert (H7 :  exists x : R, E x).
 elim H5; clear H5; intros; exists (Rmin x0 (M - m)); unfold E in |- *; intros;
  split.
 split.
@@ -1633,11 +1633,11 @@ apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ].
 assert (H8 := completeness _ H6 H7); elim H8; clear H8; intros;
  cut (0 < x1 <= M - m).
 intro; elim H8; clear H8; intros; exists (mkposreal _ H8); split.
-intros; cut ( exists alp : R | Rabs (z - x) < alp <= x1 /\ E alp).
+intros; cut (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp).
 intros; elim H11; intros; elim H12; clear H12; intros; unfold E in H13;
  elim H13; intros; apply H15.
 elim H12; intros; assumption.
-elim (classic ( exists alp : R | Rabs (z - x) < alp <= x1 /\ E alp)); intro.
+elim (classic (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp)); intro.
 assumption.
 assert
  (H12 :=
@@ -1703,8 +1703,8 @@ elim (H0 _ H3); intros DF H4; unfold covering_finite in H4; elim H4; clear H4;
  cut
   (forall x:R,
      In x l ->
-      exists del : R
-     | 0 < del /\
+      exists del : R,
+       0 < del /\
        (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\
        included (g x) (fun z:R => Rabs (z - x) < del / 2)).
 intros;
@@ -1769,7 +1769,7 @@ intros; elim (H5 x); intros; elim (H8 H6); intros;
 unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *;
  unfold E in |- *; intros; elim H11; clear H11; intros H11 _; 
  elim H11; clear H11; intros _ H11; apply H11.
-assert (H12 :  exists x : R | E x).
+assert (H12 :  exists x : R, E x).
 assert (H13 := H _ H9); unfold continuity_pt in H13;
  unfold continue_in in H13; unfold limit1_in in H13; 
  unfold limit_in in H13; simpl in H13; unfold R_dist in H13;
@@ -1791,10 +1791,10 @@ assert (H13 := completeness _ H11 H12); elim H13; clear H13; intros;
 intro; elim H13; clear H13; intros; exists x0; split.
 assumption.
 split.
-intros; cut ( exists alp : R | Rabs (z - x) < alp <= x0 /\ E alp).
+intros; cut (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp).
 intros; elim H16; intros; elim H17; clear H17; intros; unfold E in H18;
  elim H18; intros; apply H20; elim H17; intros; assumption.
-elim (classic ( exists alp : R | Rabs (z - x) < alp <= x0 /\ E alp)); intro.
+elim (classic (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp)); intro.
 assumption.
 assert
  (H17 :=
@@ -1822,4 +1822,4 @@ elim H12; intros; unfold E in H13; elim H13; intros H14 _; elim H14;
 apply Rlt_le_trans with x1; [ assumption | apply (H16 _ H13) ].
 apply H17; intros; unfold E in H18; elim H18; intros; elim H19; intros;
  assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 60f07f610..6cba456fb 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -1368,7 +1368,7 @@ intros; case (Rtotal_order x y); intro H4;
 Qed.
 
 (**********)
-Lemma sin_eq_0_1 : forall x:R, ( exists k : Z | x = IZR k * PI) -> sin x = 0.
+Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0.
 intros.
 elim H; intros.
 apply (Zcase_sign x0).
@@ -1446,7 +1446,7 @@ rewrite Ropp_involutive.
 reflexivity.
 Qed.
 
-Lemma sin_eq_0_0 : forall x:R, sin x = 0 ->  exists k : Z | x = IZR k * PI.
+Lemma sin_eq_0_0 : forall x:R, sin x = 0 ->  exists k : Z, x = IZR k * PI.
 intros.
 assert (H0 := euclidian_division x PI PI_neq0).
 elim H0; intros q H1.
@@ -1491,7 +1491,7 @@ exists q; reflexivity.
 Qed.
 
 Lemma cos_eq_0_0 :
- forall x:R, cos x = 0 ->  exists k : Z | x = IZR k * PI + PI / 2. 
+ forall x:R, cos x = 0 ->  exists k : Z, x = IZR k * PI + PI / 2. 
 intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H);
  intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z;
  rewrite <- Z_R_minus; ring; rewrite Rmult_comm; rewrite <- H3;
@@ -1500,7 +1500,7 @@ rewrite (double_var (- PI)); unfold Rdiv in |- *; ring.
 Qed.
 
 Lemma cos_eq_0_1 :
- forall x:R, ( exists k : Z | x = IZR k * PI + PI / 2) -> cos x = 0.
+ forall x:R, (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0.
 intros x H1; rewrite cos_sin; elim H1; intros x0 H2; rewrite H2;
  replace (PI / 2 + (IZR x0 * PI + PI / 2)) with (IZR x0 * PI + PI).
 rewrite neg_sin; rewrite <- Ropp_0.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index f18e9188e..ccb79e44a 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -122,7 +122,7 @@ apply Rinv_neq_0_compat; apply INR_fact_neq_0.
 Qed.
 
 Lemma archimed_cor1 :
- forall eps:R, 0 < eps ->  exists N : nat | / INR N < eps /\ (0 < N)%nat.
+ forall eps:R, 0 < eps ->  exists N : nat, / INR N < eps /\ (0 < N)%nat.
 intros; cut (/ eps < IZR (up (/ eps))).
 intro; cut (0 <= up (/ eps))%Z.
 intro; assert (H2 := IZN _ H1); elim H2; intros; exists (max x 1).
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 1175543b6..4f6951429 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -31,7 +31,7 @@ unfold Un_growing, Un_cv in |- *; intros;
  unfold is_upper_bound in H2, H3.
 assert (H5 : forall n:nat, Un n <= x).
   intro n; apply (H2 (Un n) (Un_in_EUn Un n)).
-cut ( exists N : nat | x - eps < Un N).
+cut (exists N : nat, x - eps < Un N).
 intro H6; destruct H6 as [N H6]; exists N.
 intros n H7; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps).
 unfold Rgt in H1.
@@ -491,13 +491,13 @@ Qed.
 (**********)
 Lemma approx_maj :
  forall (Un:nat -> R) (pr:has_ub Un) (eps:R),
-   0 < eps ->  exists k : nat | Rabs (majorant Un pr - Un k) < eps.
+   0 < eps ->  exists k : nat, Rabs (majorant Un pr - Un k) < eps.
 intros.
 pose (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps).
 unfold P in |- *.
 cut
- (( exists k : nat | P k) ->
-   exists k : nat | Rabs (majorant Un pr - Un k) < eps).
+ ((exists k : nat, P k) ->
+   exists k : nat, Rabs (majorant Un pr - Un k) < eps).
 intros.
 apply H0.
 apply not_all_not_ex.
@@ -559,13 +559,13 @@ Qed.
 (**********)
 Lemma approx_min :
  forall (Un:nat -> R) (pr:has_lb Un) (eps:R),
-   0 < eps ->  exists k : nat | Rabs (minorant Un pr - Un k) < eps.
+   0 < eps ->  exists k : nat, Rabs (minorant Un pr - Un k) < eps.
 intros.
 pose (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps).
 unfold P in |- *.
 cut
- (( exists k : nat | P k) ->
-   exists k : nat | Rabs (minorant Un pr - Un k) < eps).
+ ((exists k : nat, P k) ->
+   exists k : nat, Rabs (minorant Un pr - Un k) < eps).
 intros.
 apply H0.
 apply not_all_not_ex.
@@ -710,7 +710,7 @@ Qed.
 Lemma maj_by_pos :
  forall Un:nat -> R,
    sigT (fun l:R => Un_cv Un l) ->
-    exists l : R | 0 < l /\ (forall n:nat, Rabs (Un n) <= l). 
+    exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). 
 intros; elim X; intros. 
 cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). 
 intro. 
@@ -946,10 +946,10 @@ Lemma tech13 :
  forall (An:nat -> R) (k:R),
    0 <= k < 1 ->
    Un_cv (fun n:nat => Rabs (An (S n) / An n)) k ->
-    exists k0 : R
-   | k < k0 < 1 /\
-     ( exists N : nat
-      | (forall n:nat, (N <= n)%nat -> Rabs (An (S n) / An n) < k0)).
+    exists k0 : R,
+     k < k0 < 1 /\
+     (exists N : nat,
+        (forall n:nat, (N <= n)%nat -> Rabs (An (S n) / An n) < k0)).
 intros; exists (k + (1 - k) / 2).
 split.
 split.
@@ -1053,7 +1053,7 @@ Qed.
 
 (* Un -> +oo *)
 Definition cv_infty (Un:nat -> R) : Prop :=
-  forall M:R,  exists N : nat | (forall n:nat, (N <= n)%nat -> M < Un n).
+  forall M:R,  exists N : nat, (forall n:nat, (N <= n)%nat -> M < Un n).
 
 (* Un -> +oo => /Un -> O *)
 Lemma cv_infty_cv_R0 :
@@ -1117,7 +1117,7 @@ pose (Un := fun n:nat => Rabs x ^ (M_nat + n) / INR (fact (M_nat + n))).
 cut (Un_cv Un 0); unfold Un_cv in |- *; unfold R_dist in |- *; intros.
 elim (H5 eps H0); intros N H6.
 exists (M_nat + N)%nat; intros;
- cut ( exists p : nat | (p >= N)%nat /\ n = (M_nat + p)%nat).
+ cut (exists p : nat, (p >= N)%nat /\ n = (M_nat + p)%nat).
 intro; elim H8; intros p H9.
 elim H9; intros; rewrite H11; unfold Un in H6; apply H6; assumption.
 exists (n - M_nat)%nat.
@@ -1292,4 +1292,4 @@ left; apply pow_lt; apply Rabs_pos_lt; assumption.
 left; apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *;
  intro; assert (H4 := sym_eq H3); elim (fact_neq_0 _ H4).
 apply H1; assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index ffac3df29..2c035cf83 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -284,8 +284,8 @@ elim (H _ H6); clear H; intros N1 H;
  pose (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1));
  assert
   (H7 :
-    exists N : nat
-   | (forall n:nat, (N <= n)%nat -> C / sum_f_R0 An n < eps / 2))...
+    exists N : nat,
+     (forall n:nat, (N <= n)%nat -> C / sum_f_R0 An n < eps / 2))...
 case (Req_dec C 0); intro...
 exists 0%nat; intros...
 rewrite H7; unfold Rdiv in |- *; rewrite Rmult_0_l; apply Rmult_lt_0_compat...
@@ -414,4 +414,4 @@ apply sum_eq; intros; ring...
 apply H5; unfold ge in |- *; apply le_S_n; replace (S (pred n)) with n...
 apply S_pred with 0%nat; apply lt_le_trans with (S x)...
 apply lt_O_Sn...
-Qed.
\ No newline at end of file
+Qed.