Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

46 files changed, 1502 insertions, 1035 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 802bfa71..7625cce6 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(*i $Id: Alembert.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Alembert.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -25,12 +25,12 @@ Lemma Alembert_C1 :
   forall An:nat -> R,
     (forall n:nat, 0 < An n) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
 Proof.
   intros An H H0.
   cut
-    (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) ->
-      sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)).
+    ({ l:R | is_lub (EUn (fun N:nat => sum_f_R0 An N)) l } ->
+      { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }).
   intro X; apply X.
   apply completeness.
   unfold Un_cv in H0; unfold bound in |- *; cut (0 < / 2);
@@ -109,18 +109,18 @@ Proof.
   symmetry  in |- *; apply tech2; assumption.
   exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
   intro X; elim X; intros.
-  apply existT with x; apply tech10;
+  exists x; apply tech10;
     [ unfold Un_growing in |- *; intro; rewrite tech5;
       pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
 	apply Rplus_le_compat_l; left; apply H
       | apply p ].
-Qed.
+Defined.
 
 Lemma Alembert_C2 :
   forall An:nat -> R,
     (forall n:nat, An n <> 0) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
 Proof.
   intros.
   set (Vn := fun i:nat => (2 * Rabs (An i) + An i) / 2).
@@ -133,7 +133,7 @@ Proof.
   assert (H6 := Alembert_C1 Wn H2 H4).
   elim H5; intros.
   elim H6; intros.
-  apply existT with (x - x0); unfold Un_cv in |- *; unfold Un_cv in p;
+  exists (x - x0); unfold Un_cv in |- *; unfold Un_cv in p;
     unfold Un_cv in p0; intros; cut (0 < eps / 2).
   intro; elim (p (eps / 2) H8); clear p; intros.
   elim (p0 (eps / 2) H8); clear p0; intros.
@@ -334,21 +334,21 @@ Proof.
   rewrite <- Rabs_Ropp; apply RRle_abs.
   rewrite double; pattern (Rabs (An n)) at 1 in |- *; rewrite <- Rplus_0_r;
     apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H.
-Qed.
+Defined.
 
 Lemma AlembertC3_step1 :
   forall (An:nat -> R) (x:R),
     x <> 0 ->
     (forall n:nat, An n <> 0) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 ->
-    sigT (fun l:R => Pser An x l).
+    { l:R | Pser An x l }.
 Proof.
   intros; set (Bn := fun i:nat => An i * x ^ i).
   cut (forall n:nat, Bn n <> 0).
   intro; cut (Un_cv (fun n:nat => Rabs (Bn (S n) / Bn n)) 0).
   intro; assert (H4 := Alembert_C2 Bn H2 H3).
   elim H4; intros.
-  apply existT with x0; unfold Bn in p; apply tech12; assumption.
+  exists x0; unfold Bn in p; apply tech12; assumption.
   unfold Un_cv in |- *; intros; unfold Un_cv in H1; cut (0 < eps / Rabs x).
   intro; elim (H1 (eps / Rabs x) H4); intros.
   exists x0; intros; unfold R_dist in |- *; unfold Rminus in |- *;
@@ -379,13 +379,13 @@ Proof.
     [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ].
   intro; unfold Bn in |- *; apply prod_neq_R0;
     [ apply H0 | apply pow_nonzero; assumption ].
-Qed.
+Defined.
 
 Lemma AlembertC3_step2 :
-  forall (An:nat -> R) (x:R), x = 0 -> sigT (fun l:R => Pser An x l).
+  forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }.
 Proof.
-  intros; apply existT with (An 0%nat).
-  unfold Pser in |- *; unfold infinit_sum in |- *; intros; exists 0%nat; intros;
+  intros; exists (An 0%nat).
+  unfold Pser in |- *; unfold infinite_sum in |- *; intros; exists 0%nat; intros;
     replace (sum_f_R0 (fun n0:nat => An n0 * x ^ n0) n) with (An 0%nat).
   unfold R_dist in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r;
     rewrite Rabs_R0; assumption.
@@ -395,12 +395,12 @@ Proof.
     [ rewrite H; simpl in |- *; ring | unfold ge in |- *; apply le_O_n ].
 Qed.
 
-(** An useful criterion of convergence for power series *)
+(** A useful criterion of convergence for power series *)
 Theorem Alembert_C3 :
   forall (An:nat -> R) (x:R),
     (forall n:nat, An n <> 0) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 ->
-    sigT (fun l:R => Pser An x l).
+    { l:R | Pser An x l }.
 Proof.
   intros; case (total_order_T x 0); intro.
   elim s; intro.
@@ -411,19 +411,19 @@ Proof.
   cut (x <> 0).
   intro; apply AlembertC3_step1; assumption.
   red in |- *; intro; rewrite H1 in r; elim (Rlt_irrefl _ r).
-Qed.
+Defined.
 
 Lemma Alembert_C4 :
   forall (An:nat -> R) (k:R),
     0 <= k < 1 ->
     (forall n:nat, 0 < An n) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) k ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
 Proof.
   intros An k Hyp H H0.
   cut
-    (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) ->
-      sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)).
+    ({ l:R | is_lub (EUn (fun N:nat => sum_f_R0 An N)) l } ->
+      { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }).
   intro X; apply X.
   apply completeness.
   assert (H1 := tech13 _ _ Hyp H0).
@@ -524,7 +524,7 @@ Proof.
   symmetry  in |- *; apply tech2; assumption.
   exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
   intro X; elim X; intros.
-  apply existT with x; apply tech10;
+  exists x; apply tech10;
     [ unfold Un_growing in |- *; intro; rewrite tech5;
       pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
 	apply Rplus_le_compat_l; left; apply H
@@ -536,21 +536,19 @@ Lemma Alembert_C5 :
     0 <= k < 1 ->
     (forall n:nat, An n <> 0) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) k ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
 Proof.
   intros.
   cut
-    (sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l) ->
-      sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)).
+    ({ l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } ->
+      { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }).
   intro Hyp0; apply Hyp0.
   apply cv_cauchy_2.
   apply cauchy_abs.
   apply cv_cauchy_1.
   cut
-    (sigT
-      (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l) ->
-      sigT
-      (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l)).
+    ({ l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l } ->
+      { l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l }).
   intro Hyp; apply Hyp.
   apply (Alembert_C4 (fun i:nat => Rabs (An i)) k).
   assumption.
@@ -568,11 +566,11 @@ Proof.
   apply H0.
   intro X.
   elim X; intros.
-  apply existT with x.
+  exists x.
   assumption.
   intro X.
   elim X; intros.
-  apply existT with x.
+  exists x.
   assumption.
 Qed.
 
@@ -583,14 +581,12 @@ Lemma Alembert_C6 :
     0 < k ->
     (forall n:nat, An n <> 0) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) k ->
-    Rabs x < / k -> sigT (fun l:R => Pser An x l).
+    Rabs x < / k -> { l:R | Pser An x l }.
   intros.
-  cut
-    (sigT
-      (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l)).
+  cut { l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l }.
   intro X.
   elim X; intros.
-  apply existT with x0.
+  exists x0.
   apply tech12; assumption.
   case (total_order_T x 0); intro.
   elim s; intro.
@@ -655,7 +651,7 @@ Lemma Alembert_C6 :
   assumption.
   apply Rinv_0_lt_compat; apply Rabs_pos_lt.
   red in |- *; intro H7; rewrite H7 in a; elim (Rlt_irrefl _ a).
-  apply existT with (An 0%nat).
+  exists (An 0%nat).
   unfold Un_cv in |- *.
   intros.
   exists 0%nat.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 581c181f..5c4bbd6a 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: AltSeries.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+  (*i $Id: AltSeries.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -153,14 +153,14 @@ Lemma CV_ALT :
     Un_decreasing Un ->
     positivity_seq Un ->
     Un_cv Un 0 ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l }.
 Proof.
   intros.
   assert (H2 := CV_ALT_step0 _ H).
   assert (H3 := CV_ALT_step4 _ H H0).
   assert (X := growing_cv _ H2 H3).
   elim X; intros.
-  apply existT with x.
+  exists x.
   unfold Un_cv in |- *; unfold R_dist in |- *; unfold Un_cv in H1;
     unfold R_dist in H1; unfold Un_cv in p; unfold R_dist in p.
   intros; cut (0 < eps / 2);
@@ -220,7 +220,7 @@ Theorem alternated_series :
   forall Un:nat -> R,
     Un_decreasing Un ->
     Un_cv Un 0 ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l }.
 Proof.
   intros; apply CV_ALT.
   assumption.
@@ -408,7 +408,7 @@ Proof.
 Qed.
 
 Lemma exist_PI :
-  sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (tg_alt PI_tg) N) l).
+  { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt PI_tg) N) l }.
 Proof.
   apply alternated_series.
   apply PI_tg_decreasing.
@@ -416,9 +416,7 @@ Proof.
 Qed.
 
 (** Now, PI is defined *)
-Definition PI : R := 4 * match exist_PI with
-                           | existT a b => a
-                         end.
+Definition PI : R := 4 * (let (a,_) := exist_PI in a).
 
 (** We can get an approximation of PI with the following inequality *)
 Lemma PI_ineq :
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 7dbbd605..7327c64c 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: ArithProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+  (*i $Id: ArithProp.v 9454 2006-12-15 15:30:59Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rbasic_fun.
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 10965951..0de639e8 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -6,14 +6,16 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: Cos_plus.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+  (*i $Id: Cos_plus.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo_def.
 Require Import Cos_rel.
-Require Import Max. Open Local Scope nat_scope. Open Local Scope R_scope.
+Require Import Max.
+Open Local Scope nat_scope.
+Open Local Scope R_scope.
 
 Definition Majxy (x y:R) (n:nat) : R :=
   Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S n) / INR (fact n).
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index d410e14a..aed481c7 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(*i $Id: Cos_rel.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Cos_rel.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -263,7 +263,7 @@ assert (H := exist_cos (x * x)).
 elim H; intros. 
 assert (p_i := p). 
 unfold cos_in in p. 
-unfold cos_n, infinit_sum in p. 
+unfold cos_n, infinite_sum in p. 
 unfold R_dist in p. 
 cut (cos x = x0). 
 intro. 
@@ -295,7 +295,7 @@ assert (H := exist_cos ((x + y) * (x + y))).
 elim H; intros. 
 assert (p_i := p). 
 unfold cos_in in p. 
-unfold cos_n, infinit_sum in p. 
+unfold cos_n, infinite_sum in p. 
 unfold R_dist in p. 
 cut (cos (x + y) = x0). 
 intro. 
@@ -344,7 +344,7 @@ assert (H0 := exist_sin (x * x)).
 elim H0; intros. 
 assert (p_i := p). 
 unfold sin_in in p. 
-unfold sin_n, infinit_sum in p. 
+unfold sin_n, infinite_sum in p. 
 unfold R_dist in p. 
 cut (sin x = x * x0). 
 intro. 
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index a16af05c..22a52e67 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -6,10 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i        $Id: DiscrR.v 9178 2006-09-26 11:18:22Z barras $       i*)
+(*i        $Id: DiscrR.v 10710 2008-03-23 09:24:09Z herbelin $       i*)
 
 Require Import RIneq.
-Require Import Omega. Open Local Scope R_scope.
+Require Import Omega.
+Open Local Scope R_scope.
 
 Lemma Rlt_R0_R2 : 0 < 2.
 change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index beb4b744..bf729526 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Exp_prop.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Exp_prop.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -27,7 +27,7 @@ Lemma E1_cvg : forall x:R, Un_cv (E1 x) (exp x).
 Proof.
   intro; unfold exp in |- *; unfold projT1 in |- *.
   case (exist_exp x); intro.
-  unfold exp_in, Un_cv in |- *; unfold infinit_sum, E1 in |- *; trivial.
+  unfold exp_in, Un_cv in |- *; unfold infinite_sum, E1 in |- *; trivial.
 Qed.
 
 Definition Reste_E (x y:R) (N:nat) : R :=
@@ -734,7 +734,7 @@ Proof.
   apply Rinv_0_lt_compat; apply INR_fact_lt_0.
   apply (pow_lt _ n H).
   unfold exp in |- *; unfold projT1 in |- *; case (exist_exp x); intro.
-  unfold exp_in in |- *; unfold infinit_sum, Un_cv in |- *; trivial.
+  unfold exp_in in |- *; unfold infinite_sum, Un_cv in |- *; trivial.
 Qed.
 
 (**********)
@@ -769,7 +769,7 @@ Proof.
   unfold derivable_pt_lim in |- *; intros.
   set (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))).
   cut (CVN_R fn).
-  intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)).
+  intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }).
   intro cv; cut (forall n:nat, continuity (fn n)).
   intro; cut (continuity (SFL fn cv)).
   intro; unfold continuity in H1.
@@ -809,13 +809,12 @@ Proof.
   unfold Rdiv in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity.
   apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H9 ].
   unfold SFL, exp in |- *.
-  unfold projT1 in |- *.
-  case (cv h); case (exist_exp h); intros.
+  case (cv h); case (exist_exp h); simpl; intros.
   eapply UL_sequence.
   apply u.
   unfold Un_cv in |- *; intros.
   unfold exp_in in e.
-  unfold infinit_sum in e.
+  unfold infinite_sum in e.
   cut (0 < eps0 * Rabs h).
   intro; elim (e _ H9); intros N0 H10.
   exists N0; intros.
@@ -871,13 +870,12 @@ Proof.
   assert (H0 := Alembert_exp).
   unfold CVN_R in |- *.
   intro; unfold CVN_r in |- *.
-  apply existT with (fun N:nat => r ^ N / INR (fact (S N))).
+  exists (fun N:nat => r ^ N / INR (fact (S N))).
   cut
-    (sigT
-      (fun l:R =>
+    { l:R |
         Un_cv
         (fun n:nat =>
-          sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l)).
+          sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l }.
   intro X.
   elim X; intros.
   exists x; intros.
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
index b33274af..3f76e77a 100644
--- a/theories/Reals/LegacyRfield.v
+++ b/theories/Reals/LegacyRfield.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: LegacyRfield.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
 
 Require Export Raxioms.
 Require Export LegacyField.
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 8bb9298a..f22e49e1 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: MVT.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: MVT.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
-Require Import Rtopology. Open Local Scope R_scope.
+Require Import Rtopology.
+Open Local Scope R_scope.
 
 (* The Mean Value Theorem *)
 Theorem MVT :
@@ -189,7 +190,7 @@ Proof.
   intros; apply derivable_pt_id.
   intros; apply derivable_continuous_pt; apply X; assumption.
   intros; elim H1; intros; apply X; split; left; assumption.
-  intros; unfold derivable_pt in |- *; apply existT with (f' c); apply H0;
+  intros; unfold derivable_pt in |- *; exists (f' c); apply H0;
     apply H1.
 Qed.
 
@@ -695,11 +696,11 @@ Proof.
   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).
-  intros; unfold derivable_pt in |- *; apply existT with (f x0); elim (H x0 H3);
+  intros; unfold derivable_pt in |- *; exists (f x0); elim (H x0 H3);
     intros; eapply derive_pt_eq_1; symmetry  in |- *; 
       apply H4.
   assert (H4 : forall x:R, a <= x <= b -> derivable_pt g2 x).
-  intros; unfold derivable_pt in |- *; apply existT with (f x0);
+  intros; unfold derivable_pt in |- *; exists (f x0);
     elim (H0 x0 H4); intros; eapply derive_pt_eq_1; symmetry  in |- *; 
       apply H5.
   assert (H5 : forall x:R, a < x < b -> derivable_pt (g1 - g2) x).
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 306d5ac4..47ae149e 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -6,32 +6,31 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: NewtonInt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: NewtonInt.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo.
-Require Import Ranalysis. Open Local Scope R_scope.
+Require Import Ranalysis.
+Open Local Scope R_scope.
 
 (*******************************************)
 (*            Newton's Integral            *)
 (*******************************************)
 
 Definition Newton_integrable (f:R -> R) (a b:R) : Type :=
-  sigT (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a).
+  { g:R -> R | antiderivative f g a b \/ antiderivative f g b a }.
 
 Definition NewtonInt (f:R -> R) (a b:R) (pr:Newton_integrable f a b) : R :=
-  let g := match pr with
-             | existT a b => a
-           end in g b - g a.
+  let (g,_) := pr in g b - g a.
 
 (* If f is differentiable, then f' is Newton integrable (Tautology ?) *)
 Lemma FTCN_step1 :
   forall (f:Differential) (a b:R),
     Newton_integrable (fun x:R => derive_pt f x (cond_diff f x)) a b.
 Proof.
-  intros f a b; unfold Newton_integrable in |- *; apply existT with (d1 f);
+  intros f a b; unfold Newton_integrable in |- *; exists (d1 f);
     unfold antiderivative in |- *; intros; case (Rle_dec a b); 
       intro;
         [ left; split; [ intros; exists (cond_diff f x); reflexivity | assumption ]
@@ -52,7 +51,7 @@ Qed.
 Lemma NewtonInt_P1 : forall (f:R -> R) (a:R), Newton_integrable f a a.
 Proof.
   intros f a; unfold Newton_integrable in |- *;
-    apply existT with (fct_cte (f a) * id)%F; left;
+    exists (fct_cte (f a) * id)%F; left;
       unfold antiderivative in |- *; split.
   intros; assert (H1 : derivable_pt (fct_cte (f a) * id) x).
   apply derivable_pt_mult.
@@ -82,7 +81,7 @@ Lemma NewtonInt_P3 :
     Newton_integrable f b a.
 Proof.
   unfold Newton_integrable in |- *; intros; elim X; intros g H;
-    apply existT with g; tauto.
+    exists g; tauto.
 Defined.
 
 (* $\int_a^b f = -\int_b^a f$ *)
@@ -94,7 +93,7 @@ Proof.
   unfold NewtonInt in |- *;
     case
     (NewtonInt_P3 f a b
-      (existT
+      (exist
         (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x
         p)).
   intros; elim o; intro.
@@ -112,7 +111,7 @@ Proof.
   unfold NewtonInt in |- *;
     case
     (NewtonInt_P3 f a b
-      (existT
+      (exist
         (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x
         p)); intros; elim o; intro.
   assert (H1 := antiderivative_Ucte f x x0 b a H H0); elim H1; intros;
@@ -325,7 +324,7 @@ Proof.
           | left _ => F0 x
           | right _ => F1 x + (F0 b - F1 b)
         end) x).
-  unfold derivable_pt in |- *; apply existT with (f x); apply H7.
+  unfold derivable_pt in |- *; exists (f x); apply H7.
   exists H8; symmetry  in |- *; apply derive_pt_eq_0; apply H7.
   assert (H5 : a <= x <= b).
   split; [ assumption | right; assumption ].
@@ -370,7 +369,7 @@ Proof.
           | left _ => F0 x
           | right _ => F1 x + (F0 b - F1 b)
         end) x).
-  unfold derivable_pt in |- *; apply existT with (f x); apply H13.
+  unfold derivable_pt in |- *; exists (f x); apply H13.
   exists H14; symmetry  in |- *; apply derive_pt_eq_0; apply H13.
   assert (H5 : b <= x <= c).
   split; [ left; assumption | assumption ].
@@ -417,7 +416,7 @@ Proof.
           | left _ => F0 x
           | right _ => F1 x + (F0 b - F1 b)
         end) x).
-  unfold derivable_pt in |- *; apply existT with (f x); apply H7.
+  unfold derivable_pt in |- *; exists (f x); apply H7.
   exists H8; symmetry  in |- *; apply derive_pt_eq_0; apply H7.
 Qed.
 
@@ -482,7 +481,7 @@ Proof.
             match Rle_dec x b with
               | left _ => F0 x
               | right _ => F1 x + (F0 b - F1 b)
-            end); apply existT with g; left; unfold g in |- *;
+            end); exists g; left; unfold g in |- *;
         apply antiderivative_P2.
   elim H0; intro.
   assumption.
@@ -508,7 +507,7 @@ Proof.
   elim s0; intro.
 (* a<b & b<c *)
   unfold Newton_integrable in |- *;
-    apply existT with
+    exists
       (fun x:R =>
         match Rle_dec x b with
           | left _ => F0 x
@@ -526,7 +525,7 @@ Proof.
 (* a<b & b>c *)
   case (total_order_T a c); intro.
   elim s0; intro.
-  unfold Newton_integrable in |- *; apply existT with F0.
+  unfold Newton_integrable in |- *; exists F0.
   left.
   elim H1; intro.
   unfold antiderivative in H; elim H; clear H; intros _ H.
@@ -540,7 +539,7 @@ Proof.
   unfold antiderivative in H2; elim H2; clear H2; intros _ H2.
   elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)).
   rewrite b0; apply NewtonInt_P1.
-  unfold Newton_integrable in |- *; apply existT with F1.
+  unfold Newton_integrable in |- *; exists F1.
   right.
   elim H1; intro.
   unfold antiderivative in H; elim H; clear H; intros _ H.
@@ -560,7 +559,7 @@ Proof.
 (* a>b & b<c *)
   case (total_order_T a c); intro.
   elim s0; intro.
-  unfold Newton_integrable in |- *; apply existT with F1.
+  unfold Newton_integrable in |- *; exists F1.
   left.
   elim H1; intro.
 (*****************)
@@ -575,7 +574,7 @@ Proof.
   unfold antiderivative in H; elim H; clear H; intros _ H.
   elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)).
   rewrite b0; apply NewtonInt_P1.
-  unfold Newton_integrable in |- *; apply existT with F0.
+  unfold Newton_integrable in |- *; exists F0.
   right.
   elim H0; intro.
   unfold antiderivative in H; elim H; clear H; intros _ H.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 64b8e0af..e122a26a 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -6,14 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PSeries_reg.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: PSeries_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Ranalysis1.
 Require Import Max.
-Require Import Even. Open Local Scope R_scope.
+Require Import Even.
+Open Local Scope R_scope.
 
 Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.
 
@@ -28,25 +29,21 @@ Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R)
 
 (** Normal convergence *)
 Definition CVN_r (fn:nat -> R -> R) (r:posreal) : Type :=
-  sigT
-  (fun An:nat -> R =>
-    sigT
-    (fun l:R =>
+  { An:nat -> R &
+    { l:R |
       Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n) l /\
-      (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n))).
+      (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n) } }.
 
 Definition CVN_R (fn:nat -> R -> R) : Type := forall r:posreal, CVN_r fn r.
 
 Definition SFL (fn:nat -> R -> R)
-  (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)) 
-  (y:R) : R := match cv y with
-                 | existT a b => a
-               end.
+  (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }) 
+  (y:R) : R := let (a,_) := cv y in a.
 
 (** In a complete space, normal convergence implies uniform convergence *)
 Lemma CVN_CVU :
   forall (fn:nat -> R -> R)
-    (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
+    (cv:forall x:R, {l:R | Un_cv (fun N:nat => SP fn N x) l })
     (r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r.
 Proof.
   intros; unfold CVU in |- *; intros.
@@ -193,7 +190,7 @@ Qed.
 (** Continuity and normal convergence *)
 Lemma SFL_continuity_pt :
   forall (fn:nat -> R -> R)
-    (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
+    (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l })
     (r:posreal),
     CVN_r fn r ->
     (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y) ->
@@ -210,7 +207,7 @@ Qed.
 
 Lemma SFL_continuity :
   forall (fn:nat -> R -> R)
-    (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)),
+    (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }),
     CVN_R fn -> (forall n:nat, continuity (fn n)) -> continuity (SFL fn cv).
 Proof.
   intros; unfold continuity in |- *; intro.
@@ -229,7 +226,7 @@ Qed.
 (** As R is complete, normal convergence implies that (fn) is simply-uniformly convergent *) 
 Lemma CVN_R_CVS :
   forall fn:nat -> R -> R,
-    CVN_R fn -> forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l).
+    CVN_R fn -> forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }.
 Proof.
   intros; apply R_complete.
   unfold SP in |- *; set (An := fun N:nat => fn N x).
@@ -248,7 +245,7 @@ Proof.
     rewrite Rminus_0_r.
   pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
     apply Rlt_0_1.
-  apply existT with l.
+  exists l.
   cut (forall n:nat, 0 <= Bn n).
   intro; unfold Un_cv in H3; unfold Un_cv in |- *; intros.
   elim (H3 _ H6); intros.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index a8f72302..d5ae2aca 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PartSum.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: PartSum.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -153,7 +153,7 @@ Lemma tech12 :
     Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l ->
     Pser An x l.
 Proof.
-  intros; unfold Pser in |- *; unfold infinit_sum in |- *; unfold Un_cv in H;
+  intros; unfold Pser in |- *; unfold infinite_sum in |- *; unfold Un_cv in H;
     assumption.
 Qed. 
 
@@ -218,9 +218,9 @@ Qed.
 (* Unicity of the limit defined by convergent series *)
 Lemma uniqueness_sum :
   forall (An:nat -> R) (l1 l2:R),
-    infinit_sum An l1 -> infinit_sum An l2 -> l1 = l2.
+    infinite_sum An l1 -> infinite_sum An l2 -> l1 = l2.
 Proof.
-  unfold infinit_sum in |- *; intros.
+  unfold infinite_sum in |- *; intros.
   case (Req_dec l1 l2); intro.
   assumption.
   cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ].
@@ -450,7 +450,7 @@ Qed.
 (**********)
 Lemma cv_cauchy_1 :
   forall An:nat -> R,
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l) ->
+    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } ->
     Cauchy_crit_series An.
 Proof.
   intros An X.
@@ -481,7 +481,7 @@ Qed.
 Lemma cv_cauchy_2 :
   forall An:nat -> R,
     Cauchy_crit_series An ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
 Proof.
   intros.
   apply R_complete.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 7d98a844..19bdeccd 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RIneq.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: RIneq.v 10762 2008-04-06 16:57:31Z herbelin $ i*)
 
-(***************************************************************************)
-(**              Basic lemmas for the classical reals numbers              *)
-(***************************************************************************)
+(*********************************************************)
+(** * Basic lemmas for the classical real numbers        *)
+(*********************************************************)
 
 Require Export Raxioms.
 Require Import Rpow_def.
@@ -24,21 +24,32 @@ Open Local Scope R_scope.
 
 Implicit Type r : R.
 
-(**************************************************************************)
-(** * Relation between orders and equality                                *)
-(**************************************************************************)
+(*********************************************************)
+(** ** Relation between orders and equality              *)
+(*********************************************************)
+
+(** Reflexivity of the large order *)
+
+Lemma Rle_refl : forall r, r <= r.
+Proof.
+  intro; right; reflexivity.
+Qed.
+Hint Immediate Rle_refl: rorders.
+
+Lemma Rge_refl : forall r, r <= r.
+Proof. exact Rle_refl. Qed.
+Hint Immediate Rge_refl: rorders.
+
+(** Irreflexivity of the strict order *)
 
-(**********)
 Lemma Rlt_irrefl : forall r, ~ r < r.
 Proof.
   generalize Rlt_asym. intuition eauto.
 Qed.
 Hint Resolve Rlt_irrefl: real.
 
-Lemma Rle_refl : forall r, r <= r.
-Proof.
-  intro; right; reflexivity.
-Qed.
+Lemma Rgt_irrefl : forall r, ~ r > r.
+Proof. exact Rlt_irrefl. Qed.
 
 Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2.
 Proof.
@@ -58,7 +69,7 @@ Proof.
 Qed.
 Hint Resolve Rlt_dichotomy_converse: real.
 
-(** Reasoning by case on equalities and order *)
+(** Reasoning by case on equality and order *)
 
 (**********)
 Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2.
@@ -80,58 +91,104 @@ Proof.
   intros; generalize (total_order_T r1 r2); tauto.
 Qed.
 
+(*********************************************************)
+(** ** Relating [<], [>], [<=] and [>=]  	         *)
+(*********************************************************)
 
-(*********************************************************************************)
-(** *     Order Lemma  : relating [<], [>], [<=] and [>=]  	                 *)
-(*********************************************************************************)
+(*********************************************************)
+(** ** Order                                             *)
+(*********************************************************)
+
+(** *** Relating strict and large orders *)
 
-(**********)
 Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
 Proof.
   intros; red in |- *; tauto.
 Qed.
 Hint Resolve Rlt_le: real.
 
+Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
+Proof.
+  intros; red; tauto.
+Qed.
+
 (**********)
 Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
 Proof.
   destruct 1; red in |- *; auto with real.
 Qed.
-
 Hint Immediate Rle_ge: real.
+Hint Resolve Rle_ge: rorders.
 
-(**********)
 Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
 Proof.
   destruct 1; red in |- *; auto with real.
 Qed.
-
 Hint Resolve Rge_le: real.
+Hint Immediate Rge_le: rorders.
 
 (**********)
+Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
+Proof. 
+  trivial.
+Qed.
+Hint Resolve Rlt_gt: rorders.
+
+Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1.
+Proof.
+  trivial.
+Qed.
+Hint Immediate Rgt_lt: rorders.
+
+(**********)
+
 Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1.
 Proof.
   intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle in |- *; tauto.
 Qed.
-
 Hint Immediate Rnot_le_lt: real.
 
+Lemma Rnot_ge_gt : forall r1 r2, ~ r1 >= r2 -> r2 > r1.
+Proof. intros; red; apply Rnot_le_lt. auto with real. Qed.
+
+Lemma Rnot_le_gt : forall r1 r2, ~ r1 <= r2 -> r1 > r2.
+Proof. intros; red; apply Rnot_le_lt. auto with real. Qed.
+
 Lemma Rnot_ge_lt : forall r1 r2, ~ r1 >= r2 -> r1 < r2.
+Proof. intros; apply Rnot_le_lt. auto with real. Qed.
+
+Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1.
 Proof.
-  intros; apply Rnot_le_lt; auto with real.
+  intros r1 r2 H; destruct (Rtotal_order r1 r2) as [ | [ H0 | H0 ] ].
+    contradiction. subst; auto with rorders. auto with real.
 Qed.
 
+Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2.
+Proof. auto using Rnot_lt_le with real. Qed.
+
+Lemma Rnot_gt_ge : forall r1 r2, ~ r1 > r2 -> r2 >= r1.
+Proof. intros; eauto using Rnot_lt_le with rorders. Qed.
+
+Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2.
+Proof. eauto using Rnot_gt_ge with rorders. Qed.
+
 (**********)
 Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
 Proof.
   generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *.
   intuition eauto 3.
 Qed.
+Hint Immediate Rlt_not_le: real.
 
 Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2.
-Proof Rlt_not_le.
+Proof. exact Rlt_not_le. Qed.
 
-Hint Immediate Rlt_not_le: real.
+Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
+Proof. red; intros; eapply Rlt_not_le; eauto with real. Qed.
+Hint Immediate Rlt_not_ge: real.
+
+Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2.
+Proof. exact Rlt_not_ge. Qed.
 
 Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2.
 Proof.
@@ -139,13 +196,14 @@ Proof.
   unfold Rle in |- *; intuition.
 Qed.
 
-(**********)
-Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
-Proof.
-  generalize Rlt_not_le. unfold Rle, Rge in |- *. intuition eauto 3.
-Qed.
+Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2.
+Proof. intros; apply Rle_not_lt; auto with real. Qed.
 
-Hint Immediate Rlt_not_ge: real.
+Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> ~ r1 > r2.
+Proof. do 2 intro; apply Rle_not_lt. Qed.
+
+Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> ~ r1 > r2.
+Proof. do 2 intro; apply Rge_not_lt. Qed.
 
 (**********)
 Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
@@ -172,25 +230,51 @@ Proof.
 Qed.
 Hint Immediate Req_ge_sym: real.
 
+(** *** Asymmetry *)
+
+(** Remark: [Rlt_asym] is an axiom *)
+
+Lemma Rgt_asym : forall r1 r2:R, r1 > r2 -> ~ r2 > r1.
+Proof. do 2 intro; apply Rlt_asym. Qed.
+
+(** *** Antisymmetry *)
+
 Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
 Proof.
   intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle in |- *; intuition.
 Qed.
 Hint Resolve Rle_antisym: real.
 
+Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2.
+Proof. auto with real. Qed.
+
 (**********)
 Lemma Rle_le_eq : forall r1 r2, r1 <= r2 /\ r2 <= r1 <-> r1 = r2.
 Proof.
   intuition.
 Qed.
 
+Lemma Rge_ge_eq : forall r1 r2, r1 >= r2 /\ r2 >= r1 <-> r1 = r2.
+Proof.
+  intuition.
+Qed.
+
+(** *** Compatibility with equality *)
+
 Lemma Rlt_eq_compat :
   forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3.
 Proof.
   intros x x' y y'; intros; replace x with x'; replace y with y'; assumption.
 Qed.
 
-(**********)
+Lemma Rgt_eq_compat :
+  forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3.
+Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed.
+
+(** *** Transitivity *)
+
+(** Remark: [Rlt_trans] is an axiom *)
+
 Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3.
 Proof.
   generalize trans_eq Rlt_trans Rlt_eq_compat.
@@ -198,6 +282,12 @@ Proof.
   intuition eauto 2.
 Qed.
 
+Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.
+Proof. eauto using Rle_trans with rorders. Qed.
+
+Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.
+Proof. eauto using Rlt_trans with rorders. Qed.
+
 (**********)
 Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.
 Proof.
@@ -206,21 +296,25 @@ Proof.
   intuition eauto 2.
 Qed.
 
-(**********)
 Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3.
 Proof.
   generalize Rlt_trans Rlt_eq_compat; unfold Rle in |- *; intuition eauto 2.
 Qed.
 
+Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
+Proof. eauto using Rlt_le_trans with rorders. Qed.
+
+Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3.
+Proof. eauto using Rle_lt_trans with rorders. Qed.
+
+(** *** (Classical) decidability *)
 
-(** Decidability of the order *)
 Lemma Rlt_dec : forall r1 r2, {r1 < r2} + {~ r1 < r2}.
 Proof.
   intros; generalize (total_order_T r1 r2) (Rlt_dichotomy_converse r1 r2);
     intuition.
 Qed.
 
-(**********)
 Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}.
 Proof.
   intros r1 r2.
@@ -228,28 +322,44 @@ Proof.
   intuition eauto 4 with real.
 Qed.
 
-(**********)
 Lemma Rgt_dec : forall r1 r2, {r1 > r2} + {~ r1 > r2}.
-Proof.
-  intros; unfold Rgt in |- *; intros; apply Rlt_dec.
-Qed.
+Proof. do 2 intro; apply Rlt_dec. Qed.
 
-(**********)
 Lemma Rge_dec : forall r1 r2, {r1 >= r2} + {~ r1 >= r2}.
+Proof. intros; edestruct Rle_dec; [left|right]; eauto with rorders. Qed.
+
+Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}.
 Proof.
-  intros; generalize (Rle_dec r2 r1); intuition.
+  intros; generalize (total_order_T r1 r2); intuition.
 Qed.
 
-Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}.
+Lemma Rgt_ge_dec : forall r1 r2, {r1 > r2} + {r2 >= r1}.
+Proof. intros; edestruct Rlt_le_dec; [left|right]; eauto with rorders. Qed.
+
+Lemma Rle_lt_dec : forall r1 r2, {r1 <= r2} + {r2 < r1}.
 Proof.
   intros; generalize (total_order_T r1 r2); intuition.
 Qed.
 
+Lemma Rge_gt_dec : forall r1 r2, {r1 >= r2} + {r2 > r1}.
+Proof. intros; edestruct Rle_lt_dec; [left|right]; eauto with rorders. Qed.
+
+Lemma Rlt_or_le : forall r1 r2, r1 < r2 \/ r2 <= r1.
+Proof.
+  intros n m; elim (Rle_lt_dec m n); auto with real.
+Qed.
+
+Lemma Rgt_or_ge : forall r1 r2, r1 > r2 \/ r2 >= r1.
+Proof. intros; edestruct Rlt_or_le; [left|right]; eauto with rorders. Qed.
+
 Lemma Rle_or_lt : forall r1 r2, r1 <= r2 \/ r2 < r1.
 Proof.
   intros n m; elim (Rlt_le_dec m n); auto with real.
 Qed.
 
+Lemma Rge_or_gt : forall r1 r2, r1 >= r2 \/ r2 > r1.
+Proof. intros; edestruct Rle_or_lt; [left|right]; eauto with rorders. Qed.
+
 Lemma Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}.
 Proof.
   intros r1 r2 H; generalize (total_order_T r1 r2); intuition.
@@ -262,19 +372,11 @@ Proof.
   intros n m p q; intros; generalize (Rlt_le_dec m q); intuition.
 Qed.
 
-(****************************************************************)
-(** *      Field Lemmas                                         *)
-(* This part contains lemma involving the Fields operations     *)
-(****************************************************************)
 (*********************************************************)
-(** **   Addition                                        *)
+(** ** Addition                                          *)
 (*********************************************************)
 
-Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
-Proof.
-  split; ring.
-Qed.
-Hint Resolve Rplus_ne: real v62.
+(** Remark: [Rplus_0_l] is an axiom *)
 
 Lemma Rplus_0_r : forall r, r + 0 = r.
 Proof.
@@ -282,14 +384,22 @@ Proof.
 Qed.
 Hint Resolve Rplus_0_r: real.
 
+Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
+Proof.
+  split; ring.
+Qed.
+Hint Resolve Rplus_ne: real v62.
+
 (**********)
+
+(** Remark: [Rplus_opp_r] is an axiom *)
+
 Lemma Rplus_opp_l : forall r, - r + r = 0.
 Proof.
   intro; ring.
 Qed.
 Hint Resolve Rplus_opp_l: real.
 
-
 (**********)
 Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 = 0 -> r2 = - r1.
 Proof.
@@ -298,7 +408,6 @@ Proof.
   rewrite Rplus_assoc; rewrite H; ring.
 Qed.
 
-(*i New i*)
 Hint Resolve (f_equal (A:=R)): real.
 
 Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2.
@@ -325,9 +434,31 @@ Proof.
   intros r b; pattern r at 2 in |- *; replace r with (r + 0); eauto with real.
 Qed.
 
-(***********************************************************)       
-(** **    Multiplication                                   *)
-(***********************************************************)
+(***********)
+Lemma Rplus_eq_0_l :
+  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0.
+Proof.
+  intros a b H [H0| H0] H1; auto with real.
+    absurd (0 < a + b).
+      rewrite H1; auto with real.
+      apply Rle_lt_trans with (a + 0).
+        rewrite Rplus_0_r in |- *; assumption.
+        auto using Rplus_lt_compat_l with real.
+    rewrite <- H0, Rplus_0_r in H1; assumption.
+Qed.
+
+Lemma Rplus_eq_R0 :
+  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0.
+Proof.
+  intros a b; split.
+  apply Rplus_eq_0_l with b; auto with real.
+  apply Rplus_eq_0_l with a; auto with real.
+  rewrite Rplus_comm; auto with real.
+Qed.
+
+(*********************************************************)       
+(** ** Multiplication                                    *)
+(*********************************************************)
 
 (**********)
 Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1.
@@ -340,13 +471,13 @@ Lemma Rinv_l_sym : forall r, r <> 0 -> 1 = / r * r.
 Proof.
   intros; field; trivial.
 Qed.
+Hint Resolve Rinv_l_sym: real.
 
 Lemma Rinv_r_sym : forall r, r <> 0 -> 1 = r * / r.
 Proof.
   intros; field; trivial.
 Qed.
-Hint Resolve Rinv_l_sym Rinv_r_sym: real.
-
+Hint Resolve Rinv_r_sym: real.
 
 (**********)
 Lemma Rmult_0_r : forall r, r * 0 = 0.
@@ -382,7 +513,7 @@ Proof.
   auto with real.
 Qed.
 
-(*i OLD i*)Hint Resolve Rmult_eq_compat_l: v62.
+(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62.
 
 (**********)
 Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
@@ -423,7 +554,6 @@ Proof.
   auto with real.
 Qed.
 
-
 (**********) 
 Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0.
 Proof.
@@ -439,6 +569,10 @@ Proof.
 Qed.
 Hint Resolve Rmult_integral_contrapositive: real.
 
+Lemma Rmult_integral_contrapositive_currified : 
+  forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0.
+Proof. auto using Rmult_integral_contrapositive. Qed.
+
 (**********) 
 Lemma Rmult_plus_distr_r :
   forall r1 r2 r3, (r1 + r2) * r3 = r1 * r3 + r2 * r3.
@@ -446,11 +580,15 @@ Proof.
   intros; ring.
 Qed.
 
-(** ** Square function *)
+(*********************************************************)
+(** ** Square function                                   *)
+(*********************************************************)
 
 (***********)
 Definition Rsqr r : R := r * r.
 
+Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope.
+
 (***********)
 Lemma Rsqr_0 : Rsqr 0 = 0.
   unfold Rsqr in |- *; auto with real.
@@ -462,7 +600,7 @@ Lemma Rsqr_0_uniq : forall r, Rsqr r = 0 -> r = 0.
 Qed.
 
 (*********************************************************)
-(** **   Opposite                                        *)
+(** ** Opposite                                          *)
 (*********************************************************)
 
 (**********)
@@ -509,8 +647,9 @@ Proof.
 Qed.
 Hint Resolve Ropp_plus_distr: real.
 
-
-(** ** Opposite and multiplication *)
+(*********************************************************)
+(** ** Opposite and multiplication                       *)
+(*********************************************************)
 
 Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2).
 Proof.
@@ -530,7 +669,9 @@ Proof.
   intros; ring.
 Qed.
 
-(** ** Substraction *)
+(*********************************************************)
+(** ** Substraction                                      *)
+(*********************************************************)
 
 Lemma Rminus_0_r : forall r, r - 0 = r.
 Proof.
@@ -555,7 +696,6 @@ Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) = r1 - r2.
 Proof.
   intros; ring.
 Qed.
-Hint Resolve Ropp_minus_distr': real. 
 
 (**********)
 Lemma Rminus_diag_eq : forall r1 r2, r1 = r2 -> r1 - r2 = 0.
@@ -605,7 +745,6 @@ Proof.
 Qed.
 Hint Resolve Rminus_not_eq_right: real. 
 
-
 (**********)
 Lemma Rmult_minus_distr_l :
   forall r1 r2 r3, r1 * (r2 - r3) = r1 * r2 - r1 * r3.
@@ -613,7 +752,10 @@ Proof.
   intros; ring.
 Qed.
 
-(** ** Inverse *)
+(*********************************************************)
+(** ** Inverse                                           *)
+(*********************************************************)
+
 Lemma Rinv_1 : / 1 = 1.
 Proof.
   field.
@@ -677,28 +819,28 @@ Proof.
   ring.
 Qed.
 
-(** * Field operations and order *)
+(*********************************************************)
+(** ** Order and addition                                *)
+(*********************************************************)
+
+(** *** Compatibility *)
 
-(** ** Order and addition *)
+(** Remark: [Rplus_lt_compat_l] is an axiom *)
 
+Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
+Proof. eauto using Rplus_lt_compat_l with rorders. Qed.
+Hint Resolve Rplus_gt_compat_l: real.
+
+(**********)
 Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
 Proof.
   intros.
   rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real.
 Qed.
-
 Hint Resolve Rplus_lt_compat_r: real.
 
-(**********)
-Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
-Proof.
-  intros; cut (- r + r + r1 < - r + r + r2).
-  rewrite Rplus_opp_l.
-  elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1;
-    auto with zarith real.
-  rewrite Rplus_assoc; rewrite Rplus_assoc;
-    apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H).
-Qed.
+Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r.
+Proof. do 3 intro; apply Rplus_lt_compat_r. Qed.
 
 (**********)
 Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
@@ -708,6 +850,10 @@ Proof.
   right; rewrite <- H0; auto with zarith real.
 Qed.
 
+Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
+Proof. auto using Rplus_le_compat_l with rorders. Qed.
+Hint Resolve Rplus_ge_compat_l: real.
+
 (**********)
 Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r.
 Proof.
@@ -718,23 +864,8 @@ Qed.
 
 Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.
 
-(**********)
-Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
-Proof.
-  unfold Rle in |- *; intros; elim H; intro.
-  left; apply (Rplus_lt_reg_r r r1 r2 H0).
-  right; apply (Rplus_eq_reg_l r r1 r2 H0).
-Qed.
-
-(**********)
-Lemma sum_inequa_Rle_lt :
-  forall a x b c y d:R,
-    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
-Proof.
-  intros; split.
-  apply Rlt_le_trans with (a + y); auto with real.
-  apply Rlt_le_trans with (b + y); auto with real.
-Qed.
+Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r.
+Proof. auto using Rplus_le_compat_r with rorders. Qed.
 
 (*********)
 Lemma Rplus_lt_compat :
@@ -742,12 +873,22 @@ Lemma Rplus_lt_compat :
 Proof.
   intros; apply Rlt_trans with (r2 + r3); auto with real.
 Qed.
+Hint Immediate Rplus_lt_compat: real.
 
 Lemma Rplus_le_compat :
   forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
 Proof.
   intros; apply Rle_trans with (r2 + r3); auto with real.
 Qed.
+Hint Immediate Rplus_le_compat: real.
+
+Lemma Rplus_gt_compat :
+  forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
+Proof. auto using Rplus_lt_compat with rorders. Qed.
+
+Lemma Rplus_ge_compat :
+  forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4.
+Proof. auto using Rplus_le_compat with rorders. Qed.
 
 (*********)
 Lemma Rplus_lt_le_compat :
@@ -756,19 +897,133 @@ Proof.
   intros; apply Rlt_le_trans with (r2 + r3); auto with real.
 Qed.
 
-(*********)
 Lemma Rplus_le_lt_compat :
   forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
 Proof.
   intros; apply Rle_lt_trans with (r2 + r3); auto with real.
 Qed.
 
-Hint Immediate Rplus_lt_compat Rplus_le_compat Rplus_lt_le_compat
-  Rplus_le_lt_compat: real.
+Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real.
+
+Lemma Rplus_gt_ge_compat :
+  forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4.
+Proof. auto using Rplus_lt_le_compat with rorders. Qed.
+
+Lemma Rplus_ge_gt_compat :
+  forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
+Proof. auto using Rplus_le_lt_compat with rorders. Qed.
+
+(**********)
+Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
+Proof.
+  intros x y; intros; apply Rlt_trans with x;
+    [ assumption
+      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
+        assumption ].
+Qed.
+
+Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.
+Proof.
+  intros x y; intros; apply Rle_lt_trans with x;
+    [ assumption
+      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
+        assumption ].
+Qed.
+
+Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
+Proof.
+  intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat;
+    assumption.
+Qed.
 
-(** ** Order and Opposite *)
+Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
+Proof.
+  intros x y; intros; apply Rle_trans with x;
+    [ assumption
+      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+        assumption ].
+Qed.
 
 (**********)
+Lemma sum_inequa_Rle_lt :
+  forall a x b c y d:R,
+    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
+Proof.
+  intros; split.
+  apply Rlt_le_trans with (a + y); auto with real.
+  apply Rlt_le_trans with (b + y); auto with real.
+Qed.
+
+(** *** Cancellation *)
+
+Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
+Proof.
+  intros; cut (- r + r + r1 < - r + r + r2).
+  rewrite Rplus_opp_l.
+  elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1;
+    auto with zarith real.
+  rewrite Rplus_assoc; rewrite Rplus_assoc;
+    apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H).
+Qed.
+
+Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
+Proof.
+  unfold Rle in |- *; intros; elim H; intro.
+  left; apply (Rplus_lt_reg_r r r1 r2 H0).
+  right; apply (Rplus_eq_reg_l r r1 r2 H0).
+Qed.
+
+Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.
+Proof.
+  unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H).
+Qed.
+
+Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
+Proof.
+  intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real.
+Qed.
+
+(**********)
+Lemma Rplus_le_reg_pos_r :
+  forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3.
+Proof.
+  intros x y z; intros; apply Rle_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3.
+Proof.
+  intros x y z; intros; apply Rle_lt_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+Lemma Rplus_ge_reg_neg_r :
+  forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3.
+Proof.
+  intros x y z; intros; apply Rge_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3.
+Proof.
+  intros x y z; intros; apply Rge_gt_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+(*********************************************************)
+(** ** Order and opposite                                *)
+(*********************************************************)
+
+(** *** Contravariant compatibility *)
+
 Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
 Proof.
   unfold Rgt in |- *; intros.
@@ -781,55 +1036,44 @@ Proof.
 Qed.
 Hint Resolve Ropp_gt_lt_contravar.
 
-(**********)
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
 Proof.
   unfold Rgt in |- *; auto with real.
 Qed.
 Hint Resolve Ropp_lt_gt_contravar: real.
 
-Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
-Proof.
-  intros x y H'.
-  rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
-    auto with real.
-Qed.
-Hint Immediate Ropp_lt_cancel: real.
-
+(**********)
 Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
 Proof.
   auto with real.
 Qed.
 Hint Resolve Ropp_lt_contravar: real.
 
+Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2.
+Proof. auto with real. Qed.
+
 (**********)
 Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
 Proof.
-  unfold Rge in |- *; intros r1 r2 [H| H]; auto with real.
+  unfold Rge; intros r1 r2 [H| H]; auto with real.
 Qed.
 Hint Resolve Ropp_le_ge_contravar: real.
 
-Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
+Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
 Proof.
-  intros x y H.
-  elim H; auto with real.
-  intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
-    rewrite H1; auto with real.
+  unfold Rle; intros r1 r2 [H| H]; auto with real.
 Qed.
-Hint Immediate Ropp_le_cancel: real.
+Hint Resolve Ropp_ge_le_contravar: real.
 
+(**********)
 Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
 Proof.
   intros r1 r2 H; elim H; auto with real.
 Qed.
 Hint Resolve Ropp_le_contravar: real.
 
-(**********)
-Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
-Proof.
-  unfold Rge in |- *; intros r1 r2 [H| H]; auto with real.
-Qed.
-Hint Resolve Ropp_ge_le_contravar: real.
+Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2.
+Proof. auto using Ropp_le_contravar with real. Qed.
 
 (**********)
 Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
@@ -838,7 +1082,6 @@ Proof.
 Qed.
 Hint Resolve Ropp_0_lt_gt_contravar: real.
 
-(**********)
 Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
@@ -850,13 +1093,13 @@ Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0.
 Proof.
   intros; rewrite <- Ropp_0; auto with real.
 Qed.
+Hint Resolve Ropp_lt_gt_0_contravar: real.
 
-(**********)
 Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0.
 Proof.
   intros; rewrite <- Ropp_0; auto with real.
 Qed.
-Hint Resolve Ropp_lt_gt_0_contravar Ropp_gt_lt_0_contravar: real.
+Hint Resolve Ropp_gt_lt_0_contravar: real.
 
 (**********)
 Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r.
@@ -865,40 +1108,56 @@ Proof.
 Qed.
 Hint Resolve Ropp_0_le_ge_contravar: real.
 
-(**********)
 Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
 Qed.
 Hint Resolve Ropp_0_ge_le_contravar: real.
 
-(** ** Order and multiplication *)
+(** *** Cancellation *)
 
-Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
+Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
 Proof.
-  intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
+  intros x y H'.
+  rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
+    auto with real.
 Qed.
-Hint Resolve Rmult_lt_compat_r.
+Hint Immediate Ropp_lt_cancel: real.
 
-Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
+Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2.
+Proof. auto using Ropp_lt_cancel with rorders. Qed.
+
+Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
 Proof.
-  intros z x y H H0.
-  case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
-  rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto.
-  generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False;
-    generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); 
-      intro; apply (Rlt_irrefl (z * x)); auto.
+  intros x y H.
+  elim H; auto with real.
+  intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
+    rewrite H1; auto with real.
 Qed.
+Hint Immediate Ropp_le_cancel: real.
 
+Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2.
+Proof. auto using Ropp_le_cancel with rorders. Qed.
 
-Lemma Rmult_lt_gt_compat_neg_l :
-  forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.
+(*********************************************************)
+(** ** Order and multiplication                          *)
+(*********************************************************)
+
+(** Remark: [Rmult_lt_compat_l] is an axiom *)
+
+(** *** Covariant compatibility *)
+
+Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
 Proof.
-  intros; replace r with (- - r); auto with real.
-  rewrite (Ropp_mult_distr_l_reverse (- r));
-    rewrite (Ropp_mult_distr_l_reverse (- r)).
-  apply Ropp_lt_gt_contravar; auto with real.
+  intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
 Qed.
+Hint Resolve Rmult_lt_compat_r.
+
+Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r.
+Proof. eauto using Rmult_lt_compat_r with rorders. Qed.
+
+Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2.
+Proof. eauto using Rmult_lt_compat_l with rorders. Qed.
 
 (**********)
 Lemma Rmult_le_compat_l :
@@ -918,18 +1177,59 @@ Proof.
 Qed.
 Hint Resolve Rmult_le_compat_r: real.
 
-Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
+Lemma Rmult_ge_compat_l :
+  forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2.
+Proof. eauto using Rmult_le_compat_l with rorders. Qed.
+
+Lemma Rmult_ge_compat_r :
+  forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.
+Proof. eauto using Rmult_le_compat_r with rorders. Qed.
+
+(**********)
+Lemma Rmult_le_compat :
+  forall r1 r2 r3 r4,
+    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
 Proof.
-  intros z x y H H0; case H0; auto with real.
-  intros H1; apply Rlt_le.
-  apply Rmult_lt_reg_l with (r := z); auto.
-  intros H1; replace x with (/ z * (z * x)); auto with real.
-  replace y with (/ z * (z * y)).
-  rewrite H1; auto with real.
-  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
-  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
+  intros x y z t H' H'0 H'1 H'2.
+  apply Rle_trans with (r2 := x * t); auto with real.
+  repeat rewrite (fun x => Rmult_comm x t).
+  apply Rmult_le_compat_l; auto.
+  apply Rle_trans with z; auto.
+Qed.
+Hint Resolve Rmult_le_compat: real.
+
+Lemma Rmult_ge_compat :
+  forall r1 r2 r3 r4,
+    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
+Proof. auto with real rorders. Qed.
+
+Lemma Rmult_gt_0_lt_compat :
+  forall r1 r2 r3 r4,
+    r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+Proof.
+  intros; apply Rlt_trans with (r2 * r3); auto with real.
+Qed.
+
+(*********)
+Lemma Rmult_le_0_lt_compat :
+  forall r1 r2 r3 r4,
+    0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+Proof.
+  intros; apply Rle_lt_trans with (r2 * r3);
+    [ apply Rmult_le_compat_r; [ assumption | left; assumption ]
+      | apply Rmult_lt_compat_l;
+        [ apply Rle_lt_trans with r1; assumption | assumption ] ].
 Qed.
 
+(*********)
+Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.
+Proof. intros; replace 0 with (0 * r2); auto with real. Qed.
+
+Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0.
+Proof Rmult_lt_0_compat.
+
+(** *** Contravariant compatibility *)
+
 Lemma Rmult_le_compat_neg_l :
   forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
 Proof.
@@ -946,35 +1246,45 @@ Proof.
 Qed.
 Hint Resolve Rmult_le_ge_compat_neg_l: real.
 
-Lemma Rmult_le_compat :
-  forall r1 r2 r3 r4,
-    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
+Lemma Rmult_lt_gt_compat_neg_l :
+  forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.
 Proof.
-  intros x y z t H' H'0 H'1 H'2.
-  apply Rle_trans with (r2 := x * t); auto with real.
-  repeat rewrite (fun x => Rmult_comm x t).
-  apply Rmult_le_compat_l; auto.
-  apply Rle_trans with z; auto.
+  intros; replace r with (- - r); auto with real.
+  rewrite (Ropp_mult_distr_l_reverse (- r));
+    rewrite (Ropp_mult_distr_l_reverse (- r)).
+  apply Ropp_lt_gt_contravar; auto with real.
 Qed.
-Hint Resolve Rmult_le_compat: real.
 
-Lemma Rmult_gt_0_lt_compat :
-  forall r1 r2 r3 r4,
-    r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+(** *** Cancellation *)
+
+Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
 Proof.
-  intros; apply Rlt_trans with (r2 * r3); auto with real.
+  intros z x y H H0.
+  case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
+  rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto.
+  generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False;
+    generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); 
+      intro; apply (Rlt_irrefl (z * x)); auto.
 Qed.
 
-(*********)
-Lemma Rmult_ge_0_gt_0_lt_compat :
-  forall r1 r2 r3 r4,
-    r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
+Proof. eauto using Rmult_lt_reg_l with rorders. Qed.
+
+Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
 Proof.
-  intros; apply Rle_lt_trans with (r2 * r3); auto with real.
+  intros z x y H H0; case H0; auto with real.
+  intros H1; apply Rlt_le.
+  apply Rmult_lt_reg_l with (r := z); auto.
+  intros H1; replace x with (/ z * (z * x)); auto with real.
+  replace y with (/ z * (z * y)).
+  rewrite H1; auto with real.
+  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
+  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
 Qed.
 
-
-(** ** Order and Substractions *)
+(*********************************************************)
+(** ** Order and substraction                            *)
+(*********************************************************)
 
 Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
 Proof.
@@ -985,12 +1295,27 @@ Proof.
 Qed.
 Hint Resolve Rlt_minus: real.
 
+Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
+Proof. 
+  intros; apply (Rplus_lt_reg_r r2).
+  replace (r2 + (r1 - r2)) with r1.
+  replace (r2 + 0) with r2; auto with real.
+  ring.
+Qed.
+
 (**********)
 Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.
 Proof.
   destruct 1; unfold Rle in |- *; auto with real.
 Qed.
 
+Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
+Proof. 
+  destruct 1.
+    auto using Rgt_minus, Rgt_ge.
+    right; auto using Rminus_diag_eq with rorders.
+Qed.
+
 (**********)
 Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2.
 Proof.
@@ -999,6 +1324,14 @@ Proof.
   ring.
 Qed.
 
+Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2.
+Proof.
+  intros; replace r2 with (0 + r2); auto with real.
+  replace r1 with (r1 - r2 + r2).
+  apply Rplus_gt_compat_r; assumption.
+  ring.
+Qed.
+
 (**********)
 Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2.
 Proof.
@@ -1007,6 +1340,14 @@ Proof.
   ring.
 Qed.
 
+Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2.
+Proof.
+  intros; replace r2 with (0 + r2); auto with real.
+  replace r1 with (r1 - r2 + r2).
+  apply Rplus_ge_compat_r; assumption.
+  ring.
+Qed.
+
 (**********)
 Lemma tech_Rplus : forall r (s:R), 0 <= r -> 0 < s -> r + s <> 0.
 Proof.
@@ -1015,8 +1356,9 @@ Proof.
 Qed.
 Hint Immediate tech_Rplus: real.
 
-
-(** ** Order and the square function *)
+(*********************************************************)
+(** ** Order and square function                         *)
+(*********************************************************)
 
 Lemma Rle_0_sqr : forall r, 0 <= Rsqr r.
 Proof.
@@ -1036,7 +1378,26 @@ Proof.
 Qed.
 Hint Resolve Rle_0_sqr Rlt_0_sqr: real.
 
-(** ** Zero is less than one *)
+(***********)
+Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0.
+Proof.
+  intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b);
+    auto with real.
+Qed.
+
+Lemma Rplus_sqr_eq_0 :
+  forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0.
+Proof.
+  intros a b; split.
+  apply Rplus_sqr_eq_0_l with b; auto with real.
+  apply Rplus_sqr_eq_0_l with a; auto with real.
+  rewrite Rplus_comm; auto with real.
+Qed.
+
+(*********************************************************)
+(** ** Zero is less than one                             *)
+(*********************************************************)
+
 Lemma Rlt_0_1 : 0 < 1.
 Proof.
   replace 1 with (Rsqr 1); auto with real.
@@ -1050,7 +1411,10 @@ Proof.
   exact Rlt_0_1.
 Qed.
 
-(** ** Order and inverse *)
+(*********************************************************)
+(** ** Order and inverse                                 *)
+(*********************************************************)
+
 Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r.
 Proof.
   intros; apply Rnot_le_lt; red in |- *; intros.
@@ -1099,68 +1463,9 @@ Proof.
 Qed.
 Hint Resolve Rinv_1_lt_contravar: real.
 
-(********************************************************)        
-(** *     Greater                                       *)
-(********************************************************)
-
-(**********)
-Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2.
-Proof.
-  intros; apply Rle_antisym; auto with real.
-Qed.
-
-(**********)
-Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2.
-Proof.
-  intros; unfold Rge in |- *; elim (Rtotal_order r1 r2); intro.
-  absurd (r1 < r2); trivial.
-  case H0; auto.
-Qed.
-
-(**********)
-Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1.
-Proof.
-  intros; apply Rge_le; apply Rnot_lt_ge; assumption.
-Qed.
-
-(**********)
-Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2.
-Proof.
-  intros r1 r2 H; apply Rge_le.
-  exact (Rnot_lt_ge r2 r1 H).
-Qed.
-
-(**********)
-Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
-Proof.
-  red in |- *; auto with real.
-Qed.
-
-
-(**********)
-Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
-Proof.
-  unfold Rgt in |- *; intros; apply Rlt_le_trans with r2; auto with real.
-Qed.
-
-(**********)
-Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3.
-Proof.
-  unfold Rgt in |- *; intros; apply Rle_lt_trans with r2; auto with real.
-Qed.
-
-(**********)
-Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.
-Proof.
-  unfold Rgt in |- *; intros; apply Rlt_trans with r2; auto with real.
-Qed.
-
-(**********)
-Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.
-Proof.
-  intros; apply Rle_ge.
-  apply Rle_trans with r2; auto with real.
-Qed.
+(*********************************************************)        
+(** ** Miscellaneous                                     *)
+(*********************************************************)
 
 (**********)
 Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
@@ -1186,121 +1491,9 @@ Proof.
   pattern r1 at 2 in |- *; replace r1 with (r1 + 0); auto with real.
 Qed.
 
-(***********)
-Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
-Proof.
-  unfold Rgt in |- *; auto with real.
-Qed.
-Hint Resolve Rplus_gt_compat_l: real.
-
-(***********)
-Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.
-Proof.
-  unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H).
-Qed.
-
-(***********)
-Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
-Proof.
-  intros; apply Rle_ge; auto with real.
-Qed.
-Hint Resolve Rplus_ge_compat_l: real.
-
-(***********)
-Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
-Proof.
-  intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real.
-Qed.
-
-(***********)
-Lemma Rmult_ge_compat_r :
-  forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.
-Proof.
-  intros; apply Rle_ge; apply Rmult_le_compat_r; apply Rge_le; assumption.
-Qed.
-
-(***********)
-Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
-Proof.
-  intros; replace 0 with (r2 - r2); auto with real.
-  unfold Rgt, Rminus in |- *; auto with real.
-Qed.
-
-(*********)
-Lemma minus_Rgt : forall r1 r2, r1 - r2 > 0 -> r1 > r2.
-Proof.
-  intros; replace r2 with (r2 + 0); auto with real.
-  intros; replace r1 with (r2 + (r1 - r2)); auto with real.
-Qed.
-
-(**********)
-Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
-Proof.
-  unfold Rge in |- *; intros; elim H; intro.
-  left; apply (Rgt_minus r1 r2 H0).
-  right; apply (Rminus_diag_eq r1 r2 H0).
-Qed.
-
-(*********)
-Lemma minus_Rge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2.
-Proof.
-  intros; replace r2 with (r2 + 0); auto with real.
-  intros; replace r1 with (r2 + (r1 - r2)); auto with real.
-Qed.
-
-
-(*********)
-Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0.
-Proof.
-  unfold Rgt in |- *; intros.
-  replace 0 with (0 * r2); auto with real.
-Qed.
-
-(*********)
-Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.
-Proof Rmult_gt_0_compat.
-
-(***********)
-Lemma Rplus_eq_0_l :
-  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0.
-Proof.
-  intros a b [H| H] H0 H1; auto with real.
-  absurd (0 < a + b).
-  rewrite H1; auto with real.
-  replace 0 with (0 + 0); auto with real.
-Qed.
-
-
-Lemma Rplus_eq_R0 :
-  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0.
-Proof.
-  intros a b; split.
-  apply Rplus_eq_0_l with b; auto with real.
-  apply Rplus_eq_0_l with a; auto with real.
-  rewrite Rplus_comm; auto with real.
-Qed.
-
-
-(***********)
-Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0.
-Proof.
-  intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b);
-    auto with real.
-Qed.
-
-Lemma Rplus_sqr_eq_0 :
-  forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0.
-Proof.
-  intros a b; split.
-  apply Rplus_sqr_eq_0_l with b; auto with real.
-  apply Rplus_sqr_eq_0_l with a; auto with real.
-  rewrite Rplus_comm; auto with real.
-Qed.
-
-
-(**********************************************************) 
-(** *     Injection from [N] to [R]                       *)
-(**********************************************************)
+(*********************************************************) 
+(** ** Injection from [N] to [R]                         *)
+(*********************************************************)
 
 (**********)
 Lemma S_INR : forall n:nat, INR (S n) = INR n + 1.
@@ -1323,6 +1516,7 @@ Proof.
   repeat rewrite S_INR.
   rewrite Hrecn; ring.
 Qed.
+Hint Resolve plus_INR: real.
 
 (**********)
 Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) = INR n - INR m.
@@ -1332,6 +1526,7 @@ Proof.
   intros; repeat rewrite S_INR; simpl in |- *.
   rewrite H0; ring.
 Qed.
+Hint Resolve minus_INR: real.
 
 (*********)
 Lemma mult_INR : forall n m:nat, INR (n * m) = INR n * INR m.
@@ -1341,16 +1536,15 @@ Proof.
   intros; repeat rewrite S_INR; simpl in |- *.
   rewrite plus_INR; rewrite Hrecn; ring.
 Qed.
-
-Hint Resolve plus_INR minus_INR mult_INR: real.
+Hint Resolve mult_INR: real.
 
 (*********)
-Lemma lt_INR_0 : forall n:nat, (0 < n)%nat -> 0 < INR n.
+Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
 Proof.
   simple induction 1; intros; auto with real.
   rewrite S_INR; auto with real.
 Qed.
-Hint Resolve lt_INR_0: real.
+Hint Resolve lt_0_INR: real.
 
 Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
 Proof.
@@ -1360,20 +1554,20 @@ Proof.
 Qed.
 Hint Resolve lt_INR: real.
 
-Lemma INR_lt_1 : forall n:nat, (1 < n)%nat -> 1 < INR n.
+Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
 Proof.
   intros; replace 1 with (INR 1); auto with real.
 Qed.
-Hint Resolve INR_lt_1: real.
+Hint Resolve lt_1_INR: real.
 
 (**********)
-Lemma INR_pos : forall p:positive, 0 < INR (nat_of_P p).
+Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (nat_of_P p).
 Proof.
-  intro; apply lt_INR_0.
+  intro; apply lt_0_INR.
   simpl in |- *; auto with real.
   apply lt_O_nat_of_P.
 Qed.
-Hint Resolve INR_pos: real.
+Hint Resolve pos_INR_nat_of_P: real.
 
 (**********)
 Lemma pos_INR : forall n:nat, 0 <= INR n.
@@ -1410,25 +1604,25 @@ Qed.
 Hint Resolve le_INR: real.
 
 (**********)
-Lemma not_INR_O : forall n:nat, INR n <> 0 -> n <> 0%nat.
+Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat.
 Proof.
   red in |- *; intros n H H1.
   apply H.
   rewrite H1; trivial.
 Qed.
-Hint Immediate not_INR_O: real.
+Hint Immediate INR_not_0: real.
 
 (**********)
-Lemma not_O_INR : forall n:nat, n <> 0%nat -> INR n <> 0.
+Lemma not_0_INR : forall n:nat, n <> 0%nat -> INR n <> 0.
 Proof.
   intro n; case n.
   intro; absurd (0%nat = 0%nat); trivial.
   intros; rewrite S_INR.
   apply Rgt_not_eq; red in |- *; auto with real.
 Qed.
-Hint Resolve not_O_INR: real.
+Hint Resolve not_0_INR: real.
 
-Lemma not_nm_INR : forall n m:nat, n <> m -> INR n <> INR m.
+Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m.
 Proof.
   intros n m H; case (le_or_lt n m); intros H1.
   case (le_lt_or_eq _ _ H1); intros H2.
@@ -1436,17 +1630,17 @@ Proof.
   elimtype False; auto.
   apply sym_not_eq; apply Rlt_dichotomy_converse; auto with real.
 Qed.
-Hint Resolve not_nm_INR: real.
+Hint Resolve not_INR: real.
 
 Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m.
 Proof.
   intros; case (le_or_lt n m); intros H1.
   case (le_lt_or_eq _ _ H1); intros H2; auto.
   cut (n <> m).
-  intro H3; generalize (not_nm_INR n m H3); intro H4; elimtype False; auto.
+  intro H3; generalize (not_INR n m H3); intro H4; elimtype False; auto.
   omega.
   symmetry  in |- *; cut (m <> n).
-  intro H3; generalize (not_nm_INR m n H3); intro H4; elimtype False; auto.
+  intro H3; generalize (not_INR m n H3); intro H4; elimtype False; auto.
   omega.
 Qed.
 Hint Resolve INR_eq: real.
@@ -1465,9 +1659,9 @@ Proof.
 Qed.
 Hint Resolve not_1_INR: real.
 
-(**********************************************************) 
-(** *    Injection from [Z] to [R]                        *)
-(**********************************************************)
+(*********************************************************) 
+(** ** Injection from [Z] to [R]                         *)
+(*********************************************************)
 
 
 (**********)
@@ -1541,6 +1735,12 @@ Proof.
 Qed.
 
 (**********)
+Lemma succ_IZR : forall n:Z, IZR (Zsucc n) = IZR n + 1.
+Proof.
+  intro; change 1 with (IZR 1); unfold Zsucc; apply plus_IZR.
+Qed.
+
+(**********)
 Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
   intro z; case z; simpl in |- *; auto with real.
@@ -1554,7 +1754,7 @@ Proof.
 Qed. 
 
 (**********)
-Lemma lt_O_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
+Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
 Proof.
   intro z; case z; simpl in |- *; intros.
   absurd (0 < 0); auto with real.
@@ -1567,7 +1767,7 @@ Qed.
 Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
 Proof.
   intros z1 z2 H; apply Zlt_0_minus_lt. 
-  apply lt_O_IZR.
+  apply lt_0_IZR.
   rewrite <- Z_R_minus.
   exact (Rgt_minus (IZR z2) (IZR z1) H).
 Qed.
@@ -1578,7 +1778,7 @@ Proof.
   intro z; destruct z; simpl in |- *; intros; auto with zarith.
   case (Rlt_not_eq 0 (INR (nat_of_P p))); auto with real.
   case (Rlt_not_eq (- INR (nat_of_P p)) 0); auto with real.
-  apply Ropp_lt_gt_0_contravar. unfold Rgt in |- *; apply INR_pos.
+  apply Ropp_lt_gt_0_contravar. unfold Rgt in |- *; apply pos_INR_nat_of_P.
 Qed.
 
 (**********)
@@ -1590,17 +1790,17 @@ Proof.
 Qed.
 
 (**********)
-Lemma not_O_IZR : forall n:Z, n <> 0%Z -> IZR n <> 0.
+Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n <> 0.
 Proof.
   intros z H; red in |- *; intros H0; case H.
   apply eq_IZR; auto.
 Qed.
 
 (*********)
-Lemma le_O_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z.
+Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z.
 Proof.
   unfold Rle in |- *; intros z [H| H].
-  red in |- *; intro; apply (Zlt_le_weak 0 z (lt_O_IZR z H)); assumption.
+  red in |- *; intro; apply (Zlt_le_weak 0 z (lt_0_IZR z H)); assumption.
   rewrite (eq_IZR_R0 z); auto with zarith real.
 Qed.
 
@@ -1685,32 +1885,6 @@ Proof.
   apply H3; apply single_z_r_R1 with r; trivial.
 Qed.
 
-(*****************************************************************)
-(** * Definitions of new types                                   *)
-(*****************************************************************)
-
-Record nonnegreal : Type := mknonnegreal
-  {nonneg :> R; cond_nonneg : 0 <= nonneg}.
-
-Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
-
-Record nonposreal : Type := mknonposreal
-  {nonpos :> R; cond_nonpos : nonpos <= 0}.
-
-Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
-
-Record nonzeroreal : Type := mknonzeroreal
-  {nonzero :> R; cond_nonzero : nonzero <> 0}.
-
-(**********)
-Lemma prod_neq_R0 : forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0.
-Proof.
-  intros x y; intros; red in |- *; intro; generalize (Rmult_integral x y H1);
-    intro; elim H2; intro;
-      [ rewrite H3 in H; elim H | rewrite H3 in H0; elim H0 ]; 
-      reflexivity.
-Qed.
-
 (*********)
 Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
 Proof.
@@ -1728,67 +1902,18 @@ Proof.
   intro; rewrite <- double; unfold Rdiv in |- *; rewrite <- Rmult_assoc;
     symmetry  in |- *; apply Rinv_r_simpl_m.
   replace 2 with (INR 2);
-  [ apply not_O_INR; discriminate | unfold INR in |- *; ring ].
-Qed.
-
-(**********************************************************)
-(** * Other rules about < and <=                          *)
-(**********************************************************)
-
-Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
-Proof.
-  intros x y; intros; apply Rlt_trans with x;
-    [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
-        assumption ].
-Qed.
-
-Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.
-Proof.
-  intros x y; intros; apply Rle_lt_trans with x;
-    [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
-        assumption ].
-Qed.
-
-Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
-Proof.
-  intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat;
-    assumption.
-Qed.
-
-Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
-Proof.
-  intros x y; intros; apply Rle_trans with x;
-    [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
-        assumption ].
-Qed.
-
-Lemma plus_le_is_le : forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3.
-Proof.
-  intros x y z; intros; apply Rle_trans with (x + y);
-    [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
-      assumption
-      | assumption ].
+  [ apply not_0_INR; discriminate | unfold INR in |- *; ring ].
 Qed.
 
-Lemma plus_lt_is_lt : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3.
-Proof.
-  intros x y z; intros; apply Rle_lt_trans with (x + y);
-    [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
-      assumption
-      | assumption ].
-Qed.
+(*********************************************************)
+(** ** Other rules about < and <=                        *)
+(*********************************************************)
 
-Lemma Rmult_le_0_lt_compat :
+Lemma Rmult_ge_0_gt_0_lt_compat :
   forall r1 r2 r3 r4,
-    0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+    r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
 Proof.
-  intros; apply Rle_lt_trans with (r2 * r3);
-    [ apply Rmult_le_compat_r; [ assumption | left; assumption ]
-      | apply Rmult_lt_compat_l;
-        [ apply Rle_lt_trans with r1; assumption | assumption ] ].
+  intros; apply Rle_lt_trans with (r2 * r3); auto with real.
 Qed.
 
 Lemma le_epsilon :
@@ -1811,7 +1936,7 @@ Proof.
   rewrite Rmult_1_r; replace (2 * x) with (x + x).
   rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption.
   ring. 
-  replace 2 with (INR 2); [ apply not_O_INR; discriminate | reflexivity ].
+  replace 2 with (INR 2); [ apply not_0_INR; discriminate | reflexivity ].
   pattern y at 2 in |- *; replace y with (y / 2 + y / 2).
   unfold Rminus, Rdiv in |- *.
   repeat rewrite Rmult_plus_distr_r.
@@ -1822,12 +1947,12 @@ Proof.
   unfold Rdiv in |- *.
   rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
   replace 2 with (INR 2).
-  apply not_O_INR.
+  apply not_0_INR.
   discriminate.
   unfold INR in |- *; reflexivity.
   intro; ring.
   cut (0%nat <> 2%nat);
-    [ intro H0; generalize (lt_INR_0 2 (neq_O_lt 2 H0)); unfold INR in |- *;
+    [ intro H0; generalize (lt_0_INR 2 (neq_O_lt 2 H0)); unfold INR in |- *;
       intro; assumption
       | discriminate ].
 Qed.
@@ -1839,3 +1964,37 @@ Lemma completeness_weak :
 Proof.
   intros; elim (completeness E H H0); intros; split with x; assumption.
 Qed.
+
+(*********************************************************)
+(** * Definitions of new types                           *)
+(*********************************************************)
+
+Record nonnegreal : Type := mknonnegreal
+  {nonneg :> R; cond_nonneg : 0 <= nonneg}.
+
+Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
+
+Record nonposreal : Type := mknonposreal
+  {nonpos :> R; cond_nonpos : nonpos <= 0}.
+
+Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
+
+Record nonzeroreal : Type := mknonzeroreal
+  {nonzero :> R; cond_nonzero : nonzero <> 0}.
+
+(** Compatibility *)
+
+Notation prod_neq_R0 := Rmult_integral_contrapositive_currified (only parsing).
+Notation minus_Rgt := Rminus_gt (only parsing).
+Notation minus_Rge := Rminus_ge (only parsing).
+Notation plus_le_is_le := Rplus_le_reg_pos_r (only parsing).
+Notation plus_lt_is_lt := Rplus_lt_reg_pos_r (only parsing).
+Notation INR_lt_1 := lt_1_INR (only parsing).
+Notation lt_INR_0 := lt_0_INR (only parsing).
+Notation not_nm_INR := not_INR (only parsing).
+Notation INR_pos := pos_INR_nat_of_P (only parsing).
+Notation not_INR_O := INR_not_0 (only parsing).
+Notation not_O_INR := not_0_INR (only parsing).
+Notation not_O_IZR := not_0_IZR (only parsing).
+Notation le_O_IZR := le_0_IZR (only parsing).
+Notation lt_O_IZR := lt_0_IZR (only parsing).
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 270ea6da..17b6c60d 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -6,10 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: R_sqr.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: R_sqr.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
-Require Import Rbasic_fun. Open Local Scope R_scope.
+Require Import Rbasic_fun.
+Open Local Scope R_scope.
 
 (****************************************************)
 (** Rsqr : some results                             *)
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 736365a0..63b8940b 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -6,11 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: R_sqrt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: R_sqrt.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
-Require Import Rsqrt_def. Open Local Scope R_scope.
+Require Import Rsqrt_def.
+Open Local Scope R_scope.
 
 (** * Continuous extension of Rsqrt on R *)
 Definition sqrt (x:R) : R :=
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index d712f74b..f48ce563 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis.v 9319 2006-10-30 12:41:21Z barras $ i*)
+(*i $Id: Ranalysis.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -27,7 +27,8 @@ Require Export Rgeom.
 Require Export RList.
 Require Export Sqrt_reg.
 Require Export Ranalysis4.
-Require Export Rpower. Open Local Scope R_scope.
+Require Export Rpower.
+Open Local Scope R_scope.
 
 Axiom AppVar : R.
 
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 93a66e70..9414f7c9 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis1.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Ranalysis1.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Export Rlimit.
-Require Export Rderiv. Open Local Scope R_scope.
+Require Export Rderiv.
+Open Local Scope R_scope.
 Implicit Type f : R -> R.
 
 (****************************************************)
@@ -269,10 +270,10 @@ Definition derivable_pt_lim f (x l:R) : Prop :=
 
 Definition derivable_pt_abs f (x l:R) : Prop := derivable_pt_lim f x l.
 
-Definition derivable_pt f (x:R) := sigT (derivable_pt_abs f x).
+Definition derivable_pt f (x:R) := { l:R | derivable_pt_abs f x l }.
 Definition derivable f := forall x:R, derivable_pt f x.
 
-Definition derive_pt f (x:R) (pr:derivable_pt f x) := projT1 pr.
+Definition derive_pt f (x:R) (pr:derivable_pt f x) := proj1_sig pr.
 Definition derive f (pr:derivable f) (x:R) := derive_pt f x (pr x).
 
 Arguments Scope derivable_pt_lim [Rfun_scope R_scope].
@@ -380,9 +381,9 @@ Lemma derive_pt_eq :
     derive_pt f x pr = l <-> derivable_pt_lim f x l.
 Proof.
   intros; split.
-  intro; assert (H1 := projT2 pr); unfold derive_pt in H; rewrite H in H1;
+  intro; assert (H1 := proj2_sig pr); unfold derive_pt in H; rewrite H in H1;
     assumption.
-  intro; assert (H1 := projT2 pr); unfold derivable_pt_abs in H1.
+  intro; assert (H1 := proj2_sig pr); unfold derivable_pt_abs in H1.
   assert (H2 := uniqueness_limite _ _ _ _ H H1).
   unfold derive_pt in |- *; unfold derivable_pt_abs in |- *.
   symmetry  in |- *; assumption.
@@ -486,7 +487,7 @@ Qed.
 Lemma derivable_derive :
   forall f (x:R) (pr:derivable_pt f x),  exists l : R, derive_pt f x pr = l.
 Proof.
-  intros; exists (projT1 pr).
+  intros; exists (proj1_sig pr).
   unfold derive_pt in |- *; reflexivity.
 Qed.
 
@@ -714,7 +715,7 @@ Proof.
   unfold derivable_pt in |- *; intros f1 f2 x X X0.
   elim X; intros.
   elim X0; intros.
-  apply existT with (x0 + x1).
+  exists (x0 + x1).
   apply derivable_pt_lim_plus; assumption.
 Qed.
 
@@ -723,7 +724,7 @@ Lemma derivable_pt_opp :
 Proof.
   unfold derivable_pt in |- *; intros f x X.
   elim X; intros.
-  apply existT with (- x0).
+  exists (- x0).
   apply derivable_pt_lim_opp; assumption.
 Qed.
 
@@ -734,7 +735,7 @@ Proof.
   unfold derivable_pt in |- *; intros f1 f2 x X X0.
   elim X; intros.
   elim X0; intros.
-  apply existT with (x0 - x1).
+  exists (x0 - x1).
   apply derivable_pt_lim_minus; assumption.
 Qed.
 
@@ -745,14 +746,14 @@ Proof.
   unfold derivable_pt in |- *; intros f1 f2 x X X0.
   elim X; intros.
   elim X0; intros.
-  apply existT with (x0 * f2 x + f1 x * x1).
+  exists (x0 * f2 x + f1 x * x1).
   apply derivable_pt_lim_mult; assumption.
 Qed.
 
 Lemma derivable_pt_const : forall a x:R, derivable_pt (fct_cte a) x.
 Proof.
   intros; unfold derivable_pt in |- *.
-  apply existT with 0.
+  exists 0.
   apply derivable_pt_lim_const.
 Qed.
 
@@ -761,7 +762,7 @@ Lemma derivable_pt_scal :
 Proof.
   unfold derivable_pt in |- *; intros f1 a x X.
   elim X; intros.
-  apply existT with (a * x0).
+  exists (a * x0).
   apply derivable_pt_lim_scal; assumption.
 Qed.
 
@@ -774,7 +775,7 @@ Qed.
 
 Lemma derivable_pt_Rsqr : forall x:R, derivable_pt Rsqr x.
 Proof.
-  unfold derivable_pt in |- *; intro; apply existT with (2 * x).
+  unfold derivable_pt in |- *; intro; exists (2 * x).
   apply derivable_pt_lim_Rsqr.
 Qed.
 
@@ -785,7 +786,7 @@ Proof.
   unfold derivable_pt in |- *; intros f1 f2 x X X0.
   elim X; intros.
   elim X0; intros.
-  apply existT with (x1 * x0).
+  exists (x1 * x0).
   apply derivable_pt_lim_comp; assumption.
 Qed.
 
@@ -860,9 +861,9 @@ Proof.
   elim H0; clear H0; intros l2 H0.
   elim H1; clear H1; intros l H1.
   rewrite H; rewrite H0; apply derive_pt_eq_0.
-  assert (H3 := projT2 pr1).
+  assert (H3 := proj2_sig pr1).
   unfold derive_pt in H; rewrite H in H3.
-  assert (H4 := projT2 pr2).
+  assert (H4 := proj2_sig pr2).
   unfold derive_pt in H0; rewrite H0 in H4.
   apply derivable_pt_lim_plus; assumption.
 Qed.
@@ -877,7 +878,7 @@ Proof.
   elim H; clear H; intros l1 H.
   elim H0; clear H0; intros l2 H0.
   rewrite H; apply derive_pt_eq_0.
-  assert (H3 := projT2 pr1).
+  assert (H3 := proj2_sig pr1).
   unfold derive_pt in H; rewrite H in H3.
   apply derivable_pt_lim_opp; assumption.
 Qed.
@@ -896,9 +897,9 @@ Proof.
   elim H0; clear H0; intros l2 H0.
   elim H1; clear H1; intros l H1.
   rewrite H; rewrite H0; apply derive_pt_eq_0.
-  assert (H3 := projT2 pr1).
+  assert (H3 := proj2_sig pr1).
   unfold derive_pt in H; rewrite H in H3.
-  assert (H4 := projT2 pr2).
+  assert (H4 := proj2_sig pr2).
   unfold derive_pt in H0; rewrite H0 in H4.
   apply derivable_pt_lim_minus; assumption.
 Qed.
@@ -917,9 +918,9 @@ Proof.
   elim H0; clear H0; intros l2 H0.
   elim H1; clear H1; intros l H1.
   rewrite H; rewrite H0; apply derive_pt_eq_0.
-  assert (H3 := projT2 pr1).
+  assert (H3 := proj2_sig pr1).
   unfold derive_pt in H; rewrite H in H3.
-  assert (H4 := projT2 pr2).
+  assert (H4 := proj2_sig pr2).
   unfold derive_pt in H0; rewrite H0 in H4.
   apply derivable_pt_lim_mult; assumption.
 Qed.
@@ -944,7 +945,7 @@ Proof.
   elim H; clear H; intros l1 H.
   elim H0; clear H0; intros l2 H0.
   rewrite H; apply derive_pt_eq_0.
-  assert (H3 := projT2 pr).
+  assert (H3 := proj2_sig pr).
   unfold derive_pt in H; rewrite H in H3.
   apply derivable_pt_lim_scal; assumption.
 Qed.
@@ -978,9 +979,9 @@ Proof.
   elim H0; clear H0; intros l2 H0.
   elim H1; clear H1; intros l H1.
   rewrite H; rewrite H0; apply derive_pt_eq_0.
-  assert (H3 := projT2 pr1).
+  assert (H3 := proj2_sig pr1).
   unfold derive_pt in H; rewrite H in H3.
-  assert (H4 := projT2 pr2).
+  assert (H4 := proj2_sig pr2).
   unfold derive_pt in H0; rewrite H0 in H4.
   apply derivable_pt_lim_comp; assumption.
 Qed.
@@ -1046,7 +1047,7 @@ Lemma derivable_pt_pow :
   forall (n:nat) (x:R), derivable_pt (fun y:R => y ^ n) x.
 Proof.
   intros; unfold derivable_pt in |- *.
-  apply existT with (INR n * x ^ pred n).
+  exists (INR n * x ^ pred n).
   apply derivable_pt_lim_pow.
 Qed.
 
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index fb89da67..54801eb7 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -6,11 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis2.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Ranalysis2.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
-Require Import Ranalysis1. Open Local Scope R_scope.
+Require Import Ranalysis1.
+Open Local Scope R_scope.
 
 (**********)
 Lemma formule :
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index f50aa2ad..180cf9d6 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis3.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Ranalysis3.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
-Require Import Ranalysis2. Open Local Scope R_scope.
+Require Import Ranalysis2.
+Open Local Scope R_scope.
 
 (** Division *)
 Theorem derivable_pt_lim_div :
@@ -23,7 +24,7 @@ Theorem derivable_pt_lim_div :
 Proof.
   intros f1 f2 x l1 l2 H H0 H1.
   cut (derivable_pt f2 x);
-    [ intro X | unfold derivable_pt in |- *; apply existT with l2; exact H0 ].
+    [ intro X | unfold derivable_pt in |- *; exists l2; exact H0 ].
   assert (H2 := continuous_neq_0 _ _ (derivable_continuous_pt _ _ X) H1).
   elim H2; clear H2; intros eps_f2 H2.
   unfold div_fct in |- *.
@@ -761,7 +762,7 @@ Proof.
   intros f1 f2 x X X0 H.
   elim X; intros.
   elim X0; intros.
-  apply existT with ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)).
+  exists ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)).
   apply derivable_pt_lim_div; assumption.
 Qed.
 
@@ -789,9 +790,9 @@ Proof.
   elim H0; clear H0; intros l2 H0.
   elim H1; clear H1; intros l H1.
   rewrite H; rewrite H0; apply derive_pt_eq_0.
-  assert (H3 := projT2 pr1).
+  assert (H3 := proj2_sig pr1).
   unfold derive_pt in H; rewrite H in H3.
-  assert (H4 := projT2 pr2).
+  assert (H4 := proj2_sig pr2).
   unfold derive_pt in H0; rewrite H0 in H4.
   apply derivable_pt_lim_div; assumption.
 Qed.
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 205c06b4..95f6d27e 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis4.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Ranalysis4.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -14,7 +14,8 @@ Require Import SeqSeries.
 Require Import Rtrigo.
 Require Import Ranalysis1.
 Require Import Ranalysis3.
-Require Import Exp_prop. Open Local Scope R_scope.
+Require Import Exp_prop.
+Open Local Scope R_scope.
 
 (**********)
 Lemma derivable_pt_inv :
@@ -28,7 +29,7 @@ Proof.
   assumption.
   assumption.
   unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros;
-    unfold derivable_pt in |- *; apply existT with x0;
+    unfold derivable_pt in |- *; exists x0;
       unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *;
         unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; 
           intros; elim (p eps H0); intros; exists x1; intros; 
@@ -164,10 +165,10 @@ Proof.
   intros.
   case (total_order_T x 0); intro.
   elim s; intro.
-  unfold derivable_pt in |- *; apply existT with (-1).
+  unfold derivable_pt in |- *; exists (-1).
   apply (Rabs_derive_2 x a).
   elim H; exact b.
-  unfold derivable_pt in |- *; apply existT with 1.
+  unfold derivable_pt in |- *; exists 1.
   apply (Rabs_derive_1 x r).
 Qed.
 
@@ -294,8 +295,8 @@ Proof.
   unfold derivable_pt in |- *.
   assert (H := derivable_pt_lim_finite_sum An x N).
   induction  N as [| N HrecN].
-  apply existT with 0; apply H.
-  apply existT with
+  exists 0; apply H.
+  exists
     (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N))); 
     apply H.
 Qed.
@@ -352,7 +353,7 @@ Lemma derivable_pt_exp : forall x:R, derivable_pt exp x.
 Proof.
   intro.
   unfold derivable_pt in |- *.
-  apply existT with (exp x).
+  exists (exp x).
   apply derivable_pt_lim_exp.
 Qed.
 
@@ -360,7 +361,7 @@ Lemma derivable_pt_cosh : forall x:R, derivable_pt cosh x.
 Proof.
   intro.
   unfold derivable_pt in |- *.
-  apply existT with (sinh x).
+  exists (sinh x).
   apply derivable_pt_lim_cosh.
 Qed.
 
@@ -368,7 +369,7 @@ Lemma derivable_pt_sinh : forall x:R, derivable_pt sinh x.
 Proof.
   intro.
   unfold derivable_pt in |- *.
-  apply existT with (cosh x).
+  exists (cosh x).
   apply derivable_pt_lim_sinh.
 Qed.
 
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index aaea59f4..6667d2ec 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Raxioms.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Raxioms.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 (*********************************************************)
 (**    Axiomatisation of the classical reals             *)
@@ -130,7 +130,7 @@ Definition IZR (z:Z) : R :=
 Arguments Scope IZR [Z_scope].
 
 (**********************************************************)
-(** *    [R] Archimedian                                  *)
+(** *    [R] Archimedean                                  *)
 (**********************************************************)
 
 (**********)
@@ -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) -> { m:R | is_lub E m }.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 98bd607b..a5cc9f19 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rbasic_fun.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rbasic_fun.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 (*********************************************************)
 (**          Complements for the real numbers            *)
@@ -15,7 +15,8 @@
 
 Require Import Rbase.
 Require Import R_Ifp.
-Require Import Fourier. Open Local Scope R_scope.
+Require Import Fourier.
+Open Local Scope R_scope.
 
 Implicit Type r : R.
 
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index 16e12d7f..d7fee9c5 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rcomplete.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rcomplete.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -24,7 +24,7 @@ Open Local Scope R_scope.
 (****************************************************)
 
 Theorem R_complete :
-  forall Un:nat -> R, Cauchy_crit Un -> sigT (fun l:R => Un_cv Un l).
+  forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } .
 Proof.
   intros.
   set (Vn := sequence_minorant Un (cauchy_min Un H)).
@@ -37,7 +37,7 @@ Proof.
   elim H1; intros.
   cut (x = x0).
   intros.
-  apply existT with x.
+  exists x.
   rewrite <- H2 in p0.
   unfold Un_cv in |- *.
   intros.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 330c0042..002ce8d6 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Rdefinitions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rdefinitions.v 10751 2008-04-04 10:23:35Z herbelin $ i*)
 
 
 (*********************************************************)
@@ -22,6 +22,8 @@ Delimit Scope R_scope with R.
 (* Automatically open scope R_scope for arguments of type R *)
 Bind Scope R_scope with R.
 
+Open Local Scope R_scope.
+
 Parameter R0 : R.
 Parameter R1 : R.
 Parameter Rplus : R -> R -> R.
@@ -38,33 +40,33 @@ Notation "/ x" := (Rinv x) : R_scope.
 
 Infix "<" := Rlt : R_scope.
 
-(*i*******************************************************i*)
+(***********************************************************)
 
 (**********)
-Definition Rgt (r1 r2:R) : Prop := (r2 < r1)%R.
+Definition Rgt (r1 r2:R) : Prop := r2 < r1.
 
 (**********)
-Definition Rle (r1 r2:R) : Prop := (r1 < r2)%R \/ r1 = r2.
+Definition Rle (r1 r2:R) : Prop := r1 < r2 \/ r1 = r2.
 
 (**********)
 Definition Rge (r1 r2:R) : Prop := Rgt r1 r2 \/ r1 = r2.
 
 (**********)
-Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R.
+Definition Rminus (r1 r2:R) : R := r1 + - r2.
 
 (**********)
-Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R.
+Definition Rdiv (r1 r2:R) : R := r1 * / r2.
 
 (**********)
 
 Infix "-" := Rminus : R_scope.
-Infix "/" := Rdiv : R_scope.
+Infix "/" := Rdiv   : R_scope.
 
 Infix "<=" := Rle : R_scope.
 Infix ">=" := Rge : R_scope.
-Infix ">" := Rgt : R_scope.
+Infix ">"  := Rgt : R_scope.
 
-Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.
-Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.
-Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.
-Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.
+Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope.
+Notation "x <= y < z"  := (x <= y /\ y <  z) : R_scope.
+Notation "x < y < z"   := (x <  y /\ y <  z) : R_scope.
+Notation "x < y <= z"  := (x <  y /\ y <= z) : R_scope.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index e2fd2efe..ba42bad9 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rderiv.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rderiv.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 (*********************************************************)
 (**     Definition of the derivative,continuity          *)
@@ -19,7 +19,8 @@ Require Import Rlimit.
 Require Import Fourier.
 Require Import Classical_Prop.
 Require Import Classical_Pred_Type.
-Require Import Omega. Open Local Scope R_scope.
+Require Import Omega.
+Open Local Scope R_scope.
 
 (*********)
 Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 3d1c0375..b9aec1ea 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rfunctions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rfunctions.v 10762 2008-04-06 16:57:31Z herbelin $ i*)
 
 (*i Some properties about pow and sum have been made with John Harrison i*)
 (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
@@ -349,8 +349,7 @@ Proof.
   rewrite Rabs_Rinv; auto.
   rewrite <- Rinv_pow; auto.
   rewrite RPow_abs; auto.
-  rewrite H'0; rewrite Rabs_right; auto with real.
-  apply Rle_ge; auto with real.
+  rewrite H'0; rewrite Rabs_right; auto with real rorders.
   apply Rlt_pow; auto with arith.
   rewrite Rabs_Rinv; auto.
   apply Rmult_lt_reg_l with (r := Rabs r).
@@ -786,11 +785,14 @@ Proof.
 Qed.
 
 (*******************************)
-(** *     Infinit Sum          *)
+(** *     Infinite Sum          *)
 (*******************************)
 (*********)
-Definition infinit_sum (s:nat -> R) (l:R) : Prop :=
+Definition infinite_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).
+
+(** Compatibility with previous versions *)
+Notation infinit_sum := infinite_sum (only parsing).
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index 8ac9c07f..c96ae5d6 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rgeom.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rgeom.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo.
-Require Import R_sqrt. Open Local Scope R_scope.
+Require Import R_sqrt.
+Open Local Scope R_scope.
 
 (** * Distance *)
 
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 1cba821e..8d069e2d 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RiemannInt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: RiemannInt.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rfunctions.
 Require Import SeqSeries.
@@ -15,7 +15,8 @@ Require Import Rbase.
 Require Import RiemannInt_SF.
 Require Import Classical_Prop.
 Require Import Classical_Pred_Type.
-Require Import Max. Open Local Scope R_scope.
+Require Import Max.
+Open Local Scope R_scope.
 
 Set Implicit Arguments.
 
@@ -25,13 +26,11 @@ Set Implicit Arguments.
 
 Definition Riemann_integrable (f:R -> R) (a b:R) : Type :=
   forall eps:posreal,
-    sigT
-    (fun phi:StepFun a b =>
-      sigT
-      (fun psi:StepFun a b =>
+    { phi:StepFun a b &
+      { psi:StepFun a b |
         (forall t:R,
           Rmin a b <= t <= Rmax a b -> Rabs (f t - phi t) <= psi t) /\
-        Rabs (RiemannInt_SF psi) < eps)).
+        Rabs (RiemannInt_SF psi) < eps } }.
 
 Definition phi_sequence (un:nat -> posreal) (f:R -> R) 
   (a b:R) (pr:Riemann_integrable f a b) (n:nat) := 
@@ -40,12 +39,11 @@ Definition phi_sequence (un:nat -> posreal) (f:R -> R)
 Lemma phi_sequence_prop :
   forall (un:nat -> posreal) (f:R -> R) (a b:R) (pr:Riemann_integrable f a b)
     (N:nat),
-    sigT
-    (fun psi:StepFun a b =>
+    { psi:StepFun a b |
       (forall t:R,
         Rmin a b <= t <= Rmax a b ->
         Rabs (f t - phi_sequence un pr N t) <= psi t) /\
-      Rabs (RiemannInt_SF psi) < un N).
+      Rabs (RiemannInt_SF psi) < un N }.
 Proof.
   intros; apply (projT2 (pr (un N))).
 Qed.
@@ -55,8 +53,8 @@ Lemma RiemannInt_P1 :
     Riemann_integrable f a b -> Riemann_integrable f b a.
 Proof.
   unfold Riemann_integrable in |- *; intros; elim (X eps); clear X; intros;
-    elim p; clear p; intros; apply existT with (mkStepFun (StepFun_P6 (pre x)));
-      apply existT with (mkStepFun (StepFun_P6 (pre x0))); 
+    elim p; clear p; intros; exists (mkStepFun (StepFun_P6 (pre x)));
+      exists (mkStepFun (StepFun_P6 (pre x0))); 
         elim p; clear p; intros; split.
   intros; apply (H t); elim H1; clear H1; intros; split;
     [ apply Rle_trans with (Rmin b a); try assumption; right;
@@ -90,7 +88,7 @@ Lemma RiemannInt_P2 :
     (forall n:nat,
       (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\
       Rabs (RiemannInt_SF (wn n)) < un n) ->
-    sigT (fun l:R => Un_cv (fun N:nat => RiemannInt_SF (vn N)) l).
+    { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }.
 Proof.
   intros; apply R_complete; unfold Un_cv in H; unfold Cauchy_crit in |- *;
     intros; assert (H3 : 0 < eps / 2).
@@ -143,7 +141,7 @@ Lemma RiemannInt_P3 :
     (forall n:nat,
       (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\
       Rabs (RiemannInt_SF (wn n)) < un n) ->
-    sigT (fun l:R => Un_cv (fun N:nat => RiemannInt_SF (vn N)) l).
+    { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }.
 Proof.
   intros; case (Rle_dec a b); intro.
   apply RiemannInt_P2 with f un wn; assumption.
@@ -181,7 +179,7 @@ Proof.
   rewrite Rabs_Ropp in H4; apply H4.
   apply H4.
   assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros;
-    apply existT with (- x); unfold Un_cv in |- *; unfold Un_cv in p; 
+    exists (- x); unfold Un_cv in |- *; unfold Un_cv in p; 
       intros; elim (p _ H4); intros; exists x0; intros; 
         generalize (H5 _ H6); unfold R_dist, RiemannInt_SF in |- *;
           case (Rle_dec b a); case (Rle_dec a b); intros.
@@ -205,13 +203,12 @@ Lemma RiemannInt_exists :
   forall (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) 
     (un:nat -> posreal),
     Un_cv un 0 ->
-    sigT
-    (fun l:R => Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr N)) l).
+    { l:R | Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr N)) l }.
 Proof.
   intros f; intros;
     apply RiemannInt_P3 with
-      f un (fun n:nat => projT1 (phi_sequence_prop un pr n));
-      [ apply H | intro; apply (projT2 (phi_sequence_prop un pr n)) ].
+      f un (fun n:nat => proj1_sig (phi_sequence_prop un pr n));
+      [ apply H | intro; apply (proj2_sig (phi_sequence_prop un pr n)) ].
 Qed.
 
 Lemma RiemannInt_P4 :
@@ -411,9 +408,7 @@ Qed.
 
 (**********) 
 Definition RiemannInt (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) : R :=
-  match RiemannInt_exists pr RinvN RinvN_cv with
-    | existT a' b' => a'
-  end.
+  let (a,_) := RiemannInt_exists pr RinvN RinvN_cv in a.
 
 Lemma RiemannInt_P5 :
   forall (f:R -> R) (a b:R) (pr1 pr2:Riemann_integrable f a b),
@@ -433,8 +428,7 @@ Qed.
 
 Lemma maxN :
   forall (a b:R) (del:posreal),
-    a < b ->
-    sigT (fun n:nat => a + INR n * del < b /\ b <= a + INR (S n) * del).
+    a < b -> { n:nat | a + INR n * del < b /\ b <= a + INR (S n) * del }.
 Proof.
   intros; set (I := fun n:nat => a + INR n * del < b);
     assert (H0 :  exists n : nat, I n).
@@ -478,9 +472,7 @@ Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist :=
   end.
 
 Definition max_N (a b:R) (del:posreal) (h:a < b) : nat :=
-  match maxN del h with
-    | existT N H0 => N
-  end.
+  let (N,_) := maxN del h in N.
 
 Definition SubEqui (a b:R) (del:posreal) (h:a < b) : Rlist :=
   SubEquiN (S (max_N del h)) a b del.
@@ -490,12 +482,11 @@ Lemma Heine_cor1 :
     a < b ->
     (forall x:R, a <= x <= b -> continuity_pt f x) ->
     forall eps:posreal,
-      sigT
-      (fun delta:posreal =>
+      { delta:posreal |
         delta <= b - a /\
         (forall x y:R,
           a <= x <= b ->
-          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps)).
+          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps) }.
 Proof.
   intro f; intros;
     set
@@ -520,7 +511,7 @@ Proof.
           | intros; apply H3; try assumption; apply Rlt_le_trans with (Rmin x (b - a));
             [ assumption | apply Rmin_l ] ].
   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.
+  intro; elim H4; clear H4; intros; exists (mkposreal _ H4); split.
   apply H5.
   unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6;
     set (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y));
@@ -549,22 +540,21 @@ Lemma Heine_cor2 :
   forall (f:R -> R) (a b:R),
     (forall x:R, a <= x <= b -> continuity_pt f x) ->
     forall eps:posreal,
-      sigT
-      (fun delta:posreal =>
+      { delta:posreal |
         forall x y:R,
           a <= x <= b ->
-          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps).
+          a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }.
 Proof.
   intro f; intros; case (total_order_T a b); intro.
   elim s; intro.
-  assert (H0 := Heine_cor1 a0 H eps); elim H0; intros; apply existT with x;
+  assert (H0 := Heine_cor1 a0 H eps); elim H0; intros; exists x;
     elim p; intros; apply H2; assumption.
-  apply existT with (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y);
+  exists (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y);
     [ elim H0; elim H1; intros; rewrite b0 in H3; rewrite b0 in H5;
       apply Rle_antisym; apply Rle_trans with b; assumption
       | rewrite H3; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
         apply (cond_pos eps) ].
-  apply existT with (mkposreal _ Rlt_0_1); intros; elim H0; intros;
+  exists (mkposreal _ Rlt_0_1); intros; elim H0; intros;
     elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H3 H4) r)).
 Qed.
 
@@ -664,15 +654,14 @@ Qed.
 
 Lemma SubEqui_P9 :
   forall (a b:R) (del:posreal) (f:R -> R) (h:a < b),
-    sigT
-    (fun g:StepFun a b =>
+    { g:StepFun a b |
       g b = f b /\
       (forall i:nat,
         (i < pred (Rlength (SubEqui del h)))%nat ->
         constant_D_eq g
         (co_interval (pos_Rl (SubEqui del h) i)
           (pos_Rl (SubEqui del h) (S i)))
-        (f (pos_Rl (SubEqui del h) i)))).
+        (f (pos_Rl (SubEqui del h) i))) }.
 Proof.
   intros; apply StepFun_P38;
     [ apply SubEqui_P7 | apply SubEqui_P1 | apply SubEqui_P2 ].
@@ -1003,11 +992,11 @@ Proof.
       do 2 rewrite (Rmult_comm 3); repeat rewrite Rmult_assoc;
         rewrite <- Rinv_l_sym; [ ring | discrR ]
       | discrR ].
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro;
     rewrite Rmin_comm; rewrite RmaxSym;
-      apply (projT2 (phi_sequence_prop RinvN pr2 n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr1 n)).
+      apply (proj2_sig (phi_sequence_prop RinvN pr2 n)).
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr1 n)).
 Qed.
 
 Lemma RiemannInt_P9 :
@@ -1272,11 +1261,11 @@ Proof.
       case (RiemannInt_exists pr1 RinvN RinvN_cv); intros; 
         eapply UL_sequence;
           [ apply u0
-            | set (psi1 := fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n));
-              set (psi2 := fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n));
+            | set (psi1 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n));
+              set (psi2 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n));
                 apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2;
                   [ apply RinvN_cv
-                    | intro; apply (projT2 (phi_sequence_prop RinvN pr1 n))
+                    | intro; apply (proj2_sig (phi_sequence_prop RinvN pr1 n))
                     | intro;
                       assert
                         (H1 :
@@ -1284,7 +1273,7 @@ Proof.
                             Rmin a b <= t /\ t <= Rmax a b ->
                             Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi2 n t) /\
                           Rabs (RiemannInt_SF (psi2 n)) < RinvN n);
-                        [ apply (projT2 (phi_sequence_prop RinvN pr3 n))
+                        [ apply (proj2_sig (phi_sequence_prop RinvN pr3 n))
                           | elim H1; intros; split; try assumption; intros;
                             replace (f t) with (f t + l * g t);
                             [ apply H2; assumption | rewrite H0; ring ] ]
@@ -1360,8 +1349,8 @@ Proof.
             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)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr1 n0)).
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr1 n0)).
   assert
     (H8 :
       exists psi2 : nat -> StepFun a b,
@@ -1370,8 +1359,8 @@ Proof.
             Rmin a b <= t /\ t <= Rmax a b ->
             Rabs (g t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\
           Rabs (RiemannInt_SF (psi2 n)) < RinvN n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr2 n0)).
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr2 n0)).
   assert
     (H9 :
       exists psi3 : nat -> StepFun a b,
@@ -1380,8 +1369,8 @@ Proof.
             Rmin a b <= t /\ t <= Rmax a b ->
             Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\
           Rabs (RiemannInt_SF (psi3 n)) < RinvN n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr3 n0)).
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr3 n0)).
   elim H7; clear H7; intros psi1 H7; elim H8; clear H8; intros psi2 H8; elim H9;
     clear H9; intros psi3 H9;
       replace
@@ -1552,8 +1541,8 @@ Proof.
                   Rmin a b <= t /\ t <= Rmax a b ->
                   Rabs (f t - phi_sequence RinvN pr n t) <= psi1 n t) /\
                 Rabs (RiemannInt_SF (psi1 n)) < RinvN n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr n)).
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr n)).
   elim H1; clear H1; intros psi1 H1;
     set (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c));
       set (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0));
@@ -1647,8 +1636,8 @@ Proof.
               Rmin a b <= t /\ t <= Rmax a b ->
               Rabs (Rabs (f t) - phi3 n t) <= psi3 n t) /\
             Rabs (RiemannInt_SF (psi3 n)) < RinvN n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr2 n)). 
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). 
   assert
     (H1 :
       exists psi2 : nat -> StepFun a b,
@@ -1664,8 +1653,8 @@ Proof.
           (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)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr1 n)).
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr1 n)).
   elim H1; clear H1; intros psi2 H1; split with psi2; intros; elim (H1 n);
     clear H1; intros; split; try assumption.
   intros; unfold phi2 in |- *; simpl in |- *;
@@ -1698,8 +1687,8 @@ Proof.
                 Rmin a b <= t /\ t <= Rmax a b ->
                 Rabs (f t - phi1 n t) <= psi1 n t) /\
               Rabs (RiemannInt_SF (psi1 n)) < RinvN n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr1 n)). 
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). 
   elim H1; clear H1; intros psi1 H1;
     set (phi2 := fun N:nat => phi_sequence RinvN pr2 N).
   set
@@ -1722,8 +1711,8 @@ Proof.
           (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)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr2 n)). 
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). 
   elim H2; clear H2; intros psi2 H2;
     apply RiemannInt_P11 with f RinvN phi2_m psi2 psi1; 
       try assumption. 
@@ -2378,8 +2367,8 @@ Proof.
               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)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr1 n)). 
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). 
   assert
     (H2 :
       exists psi2 : nat -> StepFun b c,
@@ -2388,8 +2377,8 @@ Proof.
             Rmin b c <= t /\ t <= Rmax b c ->
             Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\
           Rabs (RiemannInt_SF (psi2 n)) < RinvN n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr2 n)). 
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). 
   assert
     (H3 :
       exists psi3 : nat -> StepFun a c,
@@ -2398,8 +2387,8 @@ Proof.
             Rmin a c <= t /\ t <= Rmax a c ->
             Rabs (f t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\
           Rabs (RiemannInt_SF (psi3 n)) < RinvN n)).
-  split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n)); intro;
-    apply (projT2 (phi_sequence_prop RinvN pr3 n)). 
+  split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); intro;
+    apply (proj2_sig (phi_sequence_prop RinvN pr3 n)). 
   elim H1; clear H1; intros psi1 H1; elim H2; clear H2; intros psi2 H2; elim H3;
     clear H3; intros psi3 H3; assert (H := RinvN_cv); 
       unfold Un_cv in |- *; intros; assert (H4 : 0 < eps / 3).
@@ -3259,7 +3248,7 @@ Lemma RiemannInt_P30 :
   forall (f:R -> R) (a b:R),
     a <= b ->
     (forall x:R, a <= x <= b -> continuity_pt f x) ->
-    sigT (fun g:R -> R => antiderivative f g a b).
+    { g:R -> R | antiderivative f g a b }.
 Proof.
   intros; split with (primitive H (FTC_P1 H H0)); apply RiemannInt_P29.
 Qed.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 0f91d006..7a02544e 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RiemannInt_SF.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: RiemannInt_SF.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -31,7 +31,7 @@ Qed.
 Lemma Nzorn :
   forall I:nat -> Prop,
     (exists n : nat, I n) ->
-    Nbound I -> sigT (fun n:nat => I n /\ (forall i:nat, I i -> (i <= n)%nat)).
+    Nbound I -> { n:nat | I n /\ (forall i:nat, I i -> (i <= n)%nat) }.
 Proof.
   intros I H H0; set (E := fun x:R =>  exists i : nat, I i /\ INR i = x);
     assert (H1 : bound E).
@@ -133,10 +133,10 @@ Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:Rlist) :=
   (forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <> pos_Rl l (S i)).
 
 Definition is_subdivision (f:R -> R) (a b:R) (l:Rlist) : Type :=
-  sigT (fun l0:Rlist => adapted_couple f a b l l0).
+  { l0:Rlist & adapted_couple f a b l l0 }.
 
 Definition IsStepFun (f:R -> R) (a b:R) : Type :=
-  sigT (fun l:Rlist => is_subdivision f a b l).
+  { l:Rlist & is_subdivision f a b l }.
 
 (** ** Class of step functions *)
 Record StepFun (a b:R) : Type := mkStepFun
@@ -1779,13 +1779,12 @@ Lemma StepFun_P38 :
     ordered_Rlist l ->
     pos_Rl l 0 = a ->
     pos_Rl l (pred (Rlength l)) = b ->
-    sigT
-    (fun g:StepFun a b =>
+    { g:StepFun a b |
       g b = f b /\
       (forall i:nat,
         (i < pred (Rlength l))%nat ->
         constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i)))
-        (f (pos_Rl l i)))).
+        (f (pos_Rl l i))) }.
 Proof. 
   intros l a b f; generalize a; clear a; induction l. 
   intros a H H0 H1; simpl in H0; simpl in H1;
@@ -2206,21 +2205,10 @@ Lemma StepFun_P43 :
     RiemannInt_SF (mkStepFun pr1) + RiemannInt_SF (mkStepFun pr2) =
     RiemannInt_SF (mkStepFun pr3).
 Proof. 
-  intros f; intros;
-    assert
-      (H1 :
-        sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a b l l0))).
-  apply pr1.
-  assert
-    (H2 :
-      sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f b c l l0))).
-  apply pr2.
-  assert
-    (H3 :
-      sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a c l l0))).
-  apply pr3.
-  elim H1; clear H1; intros l1 [lf1 H1]; elim H2; clear H2; intros l2 [lf2 H2];
-    elim H3; clear H3; intros l3 [lf3 H3].
+  intros f; intros.
+  pose proof pr1 as (l1,(lf1,H1)).
+  pose proof pr2 as (l2,(lf2,H2)).
+  pose proof pr3 as (l3,(lf3,H3)).
   replace (RiemannInt_SF (mkStepFun pr1)) with
   match Rle_dec a b with
     | left _ => Int_SF lf1 l1
@@ -2462,7 +2450,7 @@ Proof.
         (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R),
           adapted_couple f a b l1 lf1 ->
           a <= c <= b ->
-          sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a c l l0))).
+          { l:Rlist & { l0:Rlist & adapted_couple f a c l l0 } }).
   intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X.
   apply H2.
   split; assumption.
@@ -2578,7 +2566,7 @@ Proof.
         (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R),
           adapted_couple f a b l1 lf1 ->
           a <= c <= b ->
-          sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f c b l l0))).
+          { l:Rlist & { l0:Rlist & adapted_couple f c b l l0 } }).
   intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X;
     [ apply H2 | split; assumption ].
   clear f a b c H0 H H1 H2 l1 lf1; simple induction l1.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 76579ccb..1a2fa03a 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rlimit.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rlimit.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 (*********************************************************)
 (**          Definition of the limit                     *)
@@ -16,7 +16,8 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Classical_Prop.
-Require Import Fourier. Open Local Scope R_scope.
+Require Import Fourier.
+Open Local Scope R_scope.
 
 (*******************************)
 (** *   Calculus               *)
@@ -560,9 +561,9 @@ Proof.
       | apply Rlt_le_trans with (Rmin delta1 delta2);
         [ assumption | apply Rmin_l ] ].
   change (0 < eps * (Rsqr l / 2)) in |- *; unfold Rdiv in |- *;
-    repeat rewrite Rmult_assoc; repeat apply Rmult_lt_0_compat.
+    repeat rewrite Rmult_assoc; apply Rmult_lt_0_compat.
   assumption.
-  apply Rsqr_pos_lt; assumption.
+  apply Rmult_lt_0_compat. apply Rsqr_pos_lt; assumption.
   apply Rinv_0_lt_compat; cut (0%nat <> 2%nat);
     [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *;
       intro; assumption
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
new file mode 100644
index 00000000..8aadf8f5
--- /dev/null
+++ b/theories/Reals/Rlogic.v
@@ -0,0 +1,293 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * This module proves some logical properties of the axiomatics of Reals
+
+1. Decidablity of arithmetical statements from
+   the axiom that the order of the real numbers is decidable.
+
+2. Derivability of the archimedean "axiom"
+*)
+
+(** 1- Proof of the decidablity of arithmetical statements from
+excluded middle and the axiom that the order of the real numbers is
+decidable. *)
+
+(** Assuming a decidable predicate [P n], A series is constructed whose
+[n]th term is 1/2^n if [P n] holds and 0 otherwise.  This sum reaches 2
+only if [P n] holds for all [n], otherwise the sum is less than 2.
+Comparing the sum to 2 decides if [forall n, P n] or [~forall n, P n] *)
+
+(** One can iterate this lemma and use classical logic to decide any
+statement in the arithmetical hierarchy. *)
+
+(** Contributed by Cezary Kaliszyk and Russell O'Connor *)
+
+Require Import ConstructiveEpsilon.
+Require Import Rfunctions.
+Require Import PartSum.
+Require Import SeqSeries.
+Require Import RiemannInt.
+Require Import Fourier.
+ 
+Section Arithmetical_dec.
+
+Variable P : nat -> Prop.
+Hypothesis HP : forall n, {P n} + {~P n}.
+
+Let ge_fun_sums_ge_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+intros m n f mn fpos.
+replace (sum_f_R0 f m) with (sum_f_R0 f m + 0) by ring.
+rewrite (tech2 f m n mn).
+apply Rplus_le_compat_l.
+ induction (n - S m)%nat; simpl in *.
+ apply fpos.
+replace 0 with (0 + 0) by ring.
+apply (Rplus_le_compat _ _ _ _ IHn0 (fpos (S (m + S n0)%nat))).
+Qed.
+
+Let ge_fun_sums_ge : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+intros m n f mn pos.
+ elim (le_lt_or_eq _ _ mn).
+ intro; apply ge_fun_sums_ge_lemma; assumption.
+intro H; rewrite H; auto with *.
+Qed.
+
+Let f:=fun n => (if HP n then (1/2)^n else 0)%R.
+
+Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f.
+intros e He.
+assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R).
+ apply GP_infinite.
+ apply Rabs_def1; fourier.
+assert (He':e/2 > 0) by fourier.
+destruct (X _ He') as [N HN].
+clear X.
+exists N.
+intros n m Hn Hm.
+replace e with (e/2 + e/2)%R by field.
+set (g:=(fun n0 : nat => 1 * (1 / 2) ^ n0)) in *.
+assert (R_dist (sum_f_R0 g n) (sum_f_R0 g m) < e / 2 + e / 2).
+ apply Rle_lt_trans with (R_dist (sum_f_R0 g n) 2+R_dist 2 (sum_f_R0 g m))%R.
+  apply R_dist_tri.
+ replace (/(1 - 1/2)) with 2 in HN by field.
+ cut (forall n, (n >= N)%nat -> R_dist (sum_f_R0 g n) 2 < e/2)%R.
+  intros Z.
+  apply Rplus_lt_compat.
+   apply Z; assumption.
+  rewrite R_dist_sym.
+  apply Z; assumption.
+ clear - HN He.
+ intros n Hn.
+ apply HN.
+ auto.
+eapply Rle_lt_trans;[|apply H].
+clear -ge_fun_sums_ge n.
+cut (forall n m, (m <= n)%nat -> R_dist (sum_f_R0 f n) (sum_f_R0 f m) <= R_dist (sum_f_R0 g n) (sum_f_R0 g m)).
+ intros H.
+ destruct (le_lt_dec m n).
+  apply H; assumption.
+ rewrite R_dist_sym.
+ rewrite (R_dist_sym (sum_f_R0 g n)).
+ apply H; auto with *.
+clear n m.
+intros n m Hnm.
+unfold R_dist.
+cut (forall i : nat, (1 / 2) ^ i >= 0). intro RPosPow.
+rewrite Rabs_pos_eq.
+ rewrite Rabs_pos_eq.
+  cut (sum_f_R0 g m - sum_f_R0 f m <=  sum_f_R0 g n - sum_f_R0 f n).
+   intros; fourier.
+   do 2 rewrite <- minus_sum.
+   apply (ge_fun_sums_ge m n (fun i : nat => g i - f i) Hnm).
+   intro i.
+   unfold f, g.
+   elim (HP i); intro; ring_simplify; auto with *.
+  cut (sum_f_R0 g m <= sum_f_R0 g n). 
+   intro; fourier.
+  apply (ge_fun_sums_ge m n g Hnm).
+  intro. unfold g.
+  ring_simplify.
+  apply Rge_le.
+  apply RPosPow.
+ cut (sum_f_R0 f m <= sum_f_R0 f n).
+  intro; fourier.
+ apply (ge_fun_sums_ge m n f Hnm).
+ intro; unfold f.
+ elim (HP i); intro; simpl.
+  apply Rge_le.
+  apply RPosPow.
+ auto with *.
+intro i.
+apply Rle_ge.
+apply pow_le.
+fourier.
+Qed.
+
+Lemma forall_dec : {forall n, P n} + {~forall n, P n}.
+Proof.
+destruct (cv_cauchy_2 _ cauchy_crit_geometric_dec_fun).
+ cut (2 <= x <-> forall n : nat, P n).
+ intro H.
+ elim (Rle_dec 2 x); intro X.
+ left; tauto.
+ right; tauto.
+assert (A:Rabs(1/2) < 1) by (apply Rabs_def1; fourier).
+assert (A0:=(GP_infinite (1/2) A)).
+symmetry.
+ split; intro.
+ replace 2 with (/ (1 - (1 / 2))) by field.
+ unfold Pser, infinite_sum in A0.
+ eapply Rle_cv_lim;[|unfold Un_cv; apply A0 |apply u].
+ intros n.
+ clear -n H.
+  induction n; unfold f;simpl.
+  destruct (HP 0); auto with *.
+  elim n; auto.
+ apply Rplus_le_compat; auto.
+ destruct (HP (S n)); auto with *.
+ elim n0; auto.
+intros n.
+destruct (HP n); auto.
+elim (RIneq.Rle_not_lt _ _ H).
+assert (B:0< (1/2)^n).
+ apply pow_lt.
+ fourier.
+apply Rle_lt_trans with (2-(1/2)^n);[|fourier].
+replace (/(1-1/2))%R with 2 in A0 by field.
+set (g:= fun m => if (eq_nat_dec m n) then (1/2)^n else 0).
+assert (Z:  Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
+ intros e He.
+ exists n.
+ intros a Ha.
+ replace (sum_f_R0 g a) with ((1/2)^n).
+  rewrite (R_dist_eq); assumption.
+ symmetry.
+ cut (forall a : nat, ((a >= n)%nat -> sum_f_R0 g a = (1 / 2) ^ n) /\ ((a < n)%nat -> sum_f_R0 g a = 0))%R.
+  intros H0.
+  destruct (H0 a).
+  auto.
+ clear - g.
+ induction a.
+  split;
+   intros H;
+   simpl; unfold g;
+   destruct (eq_nat_dec 0 n); try reflexivity.
+   elim f; auto with *.
+  elimtype False; omega.
+ destruct IHa as [IHa0 IHa1].
+ split;
+  intros H;
+  simpl; unfold g at 2;
+  destruct (eq_nat_dec (S a) n).
+    rewrite IHa1.
+     ring.
+    omega.
+   ring_simplify.
+   apply IHa0.
+   omega.
+  elimtype False; omega.
+ ring_simplify.
+ apply IHa1.
+ omega.
+assert (C:=CV_minus _ _ _ _ A0 Z).
+eapply Rle_cv_lim;[|apply u |apply C].
+clear - n0 B.
+intros m.
+simpl.
+induction m.
+ simpl.
+ unfold f, g.
+ destruct (eq_nat_dec 0 n).
+  destruct (HP 0).
+   elim n0.
+   congruence.
+  clear -n.
+  induction n; simpl; fourier.
+ destruct (HP); simpl; fourier.
+cut (f (S m) <= 1 * ((1 / 2) ^ (S m)) - g (S m)).
+ intros L.
+ eapply Rle_trans.
+  simpl.
+  apply Rplus_le_compat.
+   apply IHm.
+  apply L.
+ simpl; fourier.
+unfold f, g.
+destruct (eq_nat_dec (S m) n).
+ destruct (HP (S m)).
+  elim n0.
+  congruence.
+ rewrite e.
+ fourier.
+destruct (HP (S m)).
+ fourier.
+ring_simplify.
+apply pow_le.
+fourier.
+Qed.
+
+Lemma sig_forall_dec :  {n | ~P n}+{forall n, P n}.
+destruct forall_dec.
+ right; assumption.
+left.
+apply constructive_indefinite_description_nat; auto.
+ clear - HP.
+ firstorder.
+apply Classical_Pred_Type.not_all_ex_not.
+assumption.
+Qed.
+
+End Arithmetical_dec.
+
+(** 2- Derivability of the Archimedean axiom *)
+
+(* This is a standard proof (it has been taken from PlanetMath). It is
+formulated negatively so as to avoid the need for classical
+logic. Using a proof of {n | ~P n}+{forall n, P n} (the one above or a
+variant of it that does not need classical axioms) , we can in
+principle also derive [up] and its [specification] *)
+
+Theorem not_not_archimedean :
+  forall r : R, ~ (forall n : nat, (INR n <= r)%R).
+intros r H.
+set (E := fun r => exists n : nat, r = INR n).
+assert (exists x : R, E x) by
+  (exists 0%R; simpl; red; exists 0%nat; reflexivity).
+assert (bound E) by (exists r; intros x (m,H2); rewrite H2; apply H).
+destruct (completeness E) as (M,(H3,H4)); try assumption.
+set (M' := (M + -1)%R).
+assert (H2 : ~ is_upper_bound E M').
+  intro H5.
+  assert (M <= M')%R by (apply H4; exact H5).
+  apply (Rlt_not_le M M').
+    unfold M' in |- *.
+    pattern M at 2 in |- *.
+    rewrite <- Rplus_0_l.
+    pattern (0 + M)%R in |- *.
+    rewrite Rplus_comm.
+    rewrite <- (Rplus_opp_r 1).
+    apply Rplus_lt_compat_l.
+    rewrite Rplus_comm.
+    apply Rlt_plus_1.
+  assumption.
+apply H2.
+intros N (n,H7).
+rewrite H7.
+unfold M' in |- *.
+assert (H5 : (INR (S n) <= M)%R) by (apply H3; exists (S n); reflexivity).
+rewrite S_INR in H5.
+assert (H6 : (INR n + 1 + -1 <= M + -1)%R).
+  apply Rplus_le_compat_r.
+  assumption.
+rewrite Rplus_assoc in H6.
+rewrite Rplus_opp_r in H6.
+rewrite (Rplus_comm (INR n) 0) in H6.
+rewrite Rplus_0_l in H6.
+assumption.
+Qed.
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index 5bdbb76b..90ea9726 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: Rpow_def.v 10923 2008-05-12 18:25:06Z herbelin $ *)
+
 Require Import Rdefinitions.
 
 Fixpoint pow (r:R) (n:nat) {struct n} : R :=
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index cb6c59d5..adf53ef9 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rpower.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rpower.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 (*i Due to L.Thery i*) 
 
 (************************************************************)
@@ -22,7 +22,8 @@ Require Import Exp_prop.
 Require Import Rsqrt_def.
 Require Import R_sqrt.
 Require Import MVT.
-Require Import Ranalysis4. Open Local Scope R_scope.
+Require Import Ranalysis4.
+Open Local Scope R_scope.
 
 Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y).
 Proof.
@@ -90,7 +91,7 @@ Proof.
         replace (/ INR (fact n)) with (1 ^ n / INR (fact n)).
   apply (H2 _ H3).
   unfold Rdiv in |- *; rewrite pow1; rewrite Rmult_1_l; reflexivity.
-  unfold infinit_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0);
+  unfold infinite_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0);
     intros; exists x0; intros;
       replace (sum_f_R0 (fun i:nat => (-1) ^ i * / INR (fact i)) n) with
       (sum_f_R0 (fun i:nat => / INR (fact i) * (-1) ^ i) n).
@@ -150,62 +151,59 @@ Proof.
   symmetry  in |- *; apply derive_pt_eq_0; apply derivable_pt_lim_exp.
 Qed.
 
-Lemma ln_exists1 : forall y:R, 0 < y -> 1 <= y -> sigT (fun z:R => y = exp z).
+Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }.
 Proof.
-  intros; set (f := fun x:R => exp x - y); cut (f 0 <= 0).
-  intro; cut (continuity f).
-  intro; cut (0 <= f y).
-  intro; cut (f 0 * f y <= 0).
-  intro; assert (X := IVT_cor f 0 y H2 (Rlt_le _ _ H) H4); elim X; intros t H5;
-    apply existT with t; elim H5; intros; unfold f in H7;
-      apply Rminus_diag_uniq_sym; exact H7.
+  intros; set (f := fun x:R => exp x - y).
+  assert (H0 : 0 < y) by (apply Rlt_le_trans with 1; auto with real).
+  cut (f 0 <= 0); [intro H1|].
+  cut (continuity f); [intro H2|].
+  cut (0 <= f y); [intro H3|].
+  cut (f 0 * f y <= 0); [intro H4|].
+  pose proof (IVT_cor f 0 y H2 (Rlt_le _ _ H0) H4) as (t,(_,H7));
+    exists t; unfold f in H7; apply Rminus_diag_uniq_sym; exact H7.
   pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y));
     rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l; 
       assumption.
   unfold f in |- *; apply Rplus_le_reg_l with y; left;
     apply Rlt_trans with (1 + y).
   rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1.
-  replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H) | ring ].
+  replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H0) | ring ].
   unfold f in |- *; change (continuity (exp - fct_cte y)) in |- *;
     apply continuity_minus;
       [ apply derivable_continuous; apply derivable_exp
         | apply derivable_continuous; apply derivable_const ].
   unfold f in |- *; rewrite exp_0; apply Rplus_le_reg_l with y;
-    rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H0 | ring ].
+    rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H | ring ].
 Qed.
 
 (**********)
-Lemma ln_exists : forall y:R, 0 < y -> sigT (fun z:R => y = exp z).
+Lemma ln_exists : forall y:R, 0 < y -> { z:R | y = exp z }.
 Proof.
   intros; case (Rle_dec 1 y); intro.
-  apply (ln_exists1 _ H r).
+  apply (ln_exists1 _ r).
   assert (H0 : 1 <= / y).
   apply Rmult_le_reg_l with y.
   apply H.
   rewrite <- Rinv_r_sym.
   rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ n).
   red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
-  assert (H1 : 0 < / y).
-  apply Rinv_0_lt_compat; apply H.
-  assert (H2 := ln_exists1 _ H1 H0); elim H2; intros; apply existT with (- x);
+  destruct (ln_exists1 _ H0) as (x,p); exists (- x);
     apply Rmult_eq_reg_l with (exp x / y).
   unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
   rewrite Rmult_1_r; rewrite <- (Rmult_comm (/ y)); rewrite Rmult_assoc;
     rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; 
       rewrite Rmult_1_r; symmetry  in |- *; apply p.
-  red in |- *; intro; rewrite H3 in H; elim (Rlt_irrefl _ H).
+  red in |- *; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H).
   unfold Rdiv in |- *; apply prod_neq_R0.
-  assert (H3 := exp_pos x); red in |- *; intro; rewrite H4 in H3;
+  assert (H3 := exp_pos x); red in |- *; intro H4; rewrite H4 in H3;
     elim (Rlt_irrefl _ H3).
-  apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H;
+  apply Rinv_neq_0_compat; red in |- *; intro H3; rewrite H3 in H;
     elim (Rlt_irrefl _ H).
 Qed.
 
 (* Definition of log R+* -> R *)
 Definition Rln (y:posreal) : R :=
-  match ln_exists (pos y) (cond_pos y) with
-    | existT a b => a
-  end.
+  let (a,_) := ln_exists (pos y) (cond_pos y) in a.
 
 (* Extension on R *)
 Definition ln (x:R) : R :=
@@ -403,6 +401,16 @@ Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
 (** *                     Properties of  Rpower                   *)
 (******************************************************************)
 
+(** Note: [Rpower] is prolongated to [1] on negative real numbers and
+    it thus does not extend integer power. The next two lemmas, which
+    hold for integer power, accidentally hold on negative real numbers
+    as a side effect of the default value taken on negative real
+    numbers. Contrastingly, the lemmas that do not hold for the
+    integer power of a negative number are stated for [Rpower] on the
+    positive numbers only (even if they accidentally hold due to the
+    default value of [Rpower] on the negative side, as it is the case
+    for [Rpower_O]). *)
+
 Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y.
 Proof.
   intros x y z; unfold Rpower in |- *.
@@ -420,7 +428,7 @@ Qed.
 
 Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1.
 Proof.
-  intros x H; unfold Rpower in |- *.
+  intros x _; unfold Rpower in |- *.
   rewrite Rmult_0_l; apply exp_0.
 Qed.
 
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index a84d5149..2113cc8f 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rprod.v 9298 2006-10-27 13:05:29Z notin $ i*)
+(*i $Id: Rprod.v 10146 2007-09-27 12:28:12Z herbelin $ i*)
 
 Require Import Compare.
 Require Import Rbase.
@@ -16,41 +16,42 @@ Require Import PartSum.
 Require Import Binomial.
 Open Local Scope R_scope.
 
-(** TT Ak; 1<=k<=N *)
-Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R :=
+(** TT Ak; 0<=k<=N *)
+Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) {struct N} : R :=
   match N with
-    | O => 1
-    | S p => prod_f_SO An p * An (S p)
+    | O => f O
+    | S p => prod_f_R0 f p * f (S p)
   end.
 
+Notation prod_f_SO := (fun An N => prod_f_R0 (fun n => An (S n)) N).
+
 (**********)
 Lemma prod_SO_split :
   forall (An:nat -> R) (n k:nat),
-    (k <= n)%nat ->
-    prod_f_SO An n =
-    prod_f_SO An k * prod_f_SO (fun l:nat => An (k + l)%nat) (n - k).
+    (k < n)%nat ->
+    prod_f_R0 An n =
+    prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1).
 Proof.
   intros; induction  n as [| n Hrecn].
-  cut (k = 0%nat);
-    [ intro; rewrite H0; simpl in |- *; ring | inversion H; reflexivity ].
-  cut (k = S n \/ (k <= n)%nat).
-  intro; elim H0; intro.
-  rewrite H1; simpl in |- *; rewrite <- minus_n_n; simpl in |- *; ring.
-  replace (S n - k)%nat with (S (n - k)).
+  absurd (k < 0)%nat; omega.
+  cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|omega].
+  replace (S n - k - 1)%nat with O; [rewrite H1; simpl|omega].
+  replace (n+1+0)%nat with (S n); ring.
+  replace (S n - k-1)%nat with (S (n - k-1));[idtac|omega].
   simpl in |- *; replace (k + S (n - k))%nat with (S n).
+  replace (k + 1 + S (n - k - 1))%nat with (S n).
   rewrite Hrecn; [ ring | assumption ].
   omega.
   omega.
-  omega.
-Qed.
+Qed. 
 
 (**********)
 Lemma prod_SO_pos :
   forall (An:nat -> R) (N:nat),
-    (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_SO An N.
+    (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_R0 An N.
 Proof.
   intros; induction  N as [| N HrecN].
-  simpl in |- *; left; apply Rlt_0_1.
+  simpl in |- *; apply H; trivial.
   simpl in |- *; apply Rmult_le_pos.
   apply HrecN; intros; apply H; apply le_trans with N;
     [ assumption | apply le_n_Sn ].
@@ -61,11 +62,11 @@ Qed.
 Lemma prod_SO_Rle :
   forall (An Bn:nat -> R) (N:nat),
     (forall n:nat, (n <= N)%nat -> 0 <= An n <= Bn n) ->
-    prod_f_SO An N <= prod_f_SO Bn N.
+    prod_f_R0 An N <= prod_f_R0 Bn N.
 Proof.
   intros; induction  N as [| N HrecN].
-  right; reflexivity.
-  simpl in |- *; apply Rle_trans with (prod_f_SO An N * Bn (S N)).
+  elim  H with O; trivial.
+  simpl in |- *; apply Rle_trans with (prod_f_R0 An N * Bn (S N)).
   apply Rmult_le_compat_l.
   apply prod_SO_pos; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros;
     assumption.
@@ -79,12 +80,17 @@ Qed.
 
 (** Application to factorial *)
 Lemma fact_prodSO :
-  forall n:nat, INR (fact n) = prod_f_SO (fun k:nat => INR k) n.
+  forall n:nat, INR (fact n) = prod_f_R0 (fun k:nat => 
+     (match (eq_nat_dec k 0) with 
+          | left   _ => 1%R 
+          | right _ => INR k
+                        end)) n.
 Proof.
   intro; induction  n as [| n Hrecn].
   reflexivity.
-  change (INR (S n * fact n) = prod_f_SO (fun k:nat => INR k) (S n)) in |- *.
-  rewrite mult_INR; rewrite Rmult_comm; rewrite Hrecn; reflexivity.
+  simpl; rewrite <- Hrecn.
+  case n; auto with real.
+  intros; repeat rewrite plus_INR;rewrite mult_INR;ring.
 Qed.
 
 Lemma le_n_2n : forall n:nat, (n <= 2 * n)%nat.
@@ -104,40 +110,58 @@ Lemma RfactN_fact2N_factk :
     (k <= 2 * N)%nat ->
     Rsqr (INR (fact N)) <= INR (fact (2 * N - k)) * INR (fact k).
 Proof.
+  assert (forall (n:nat), 0 <= (if eq_nat_dec n 0 then 1 else INR n)).
+  intros; case (eq_nat_dec n 0); auto with real.
+  assert (forall (n:nat), (0 < n)%nat ->  
+     (if eq_nat_dec n 0 then 1 else INR n) = INR n).
+  intros n; case (eq_nat_dec n 0); auto with real.
+  intros; absurd (0 < n)%nat; omega.
   intros; unfold Rsqr in |- *; repeat rewrite fact_prodSO.
-  cut ((k <= N)%nat \/ (N <= k)%nat).
-  intro; elim H0; intro.
-  rewrite (prod_SO_split (fun l:nat => INR l) (2 * N - k) N).
+  cut ((k=N)%nat \/ (k < N)%nat \/ (N < k)%nat).
+  intro H2; elim H2; intro H3.
+  rewrite H3; replace (2*N-N)%nat with N;[right; ring|omega].
+  case H3; intro; clear H2 H3.
+  rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) (2 * N - k) N).
   rewrite Rmult_assoc; apply Rmult_le_compat_l.
-  apply prod_SO_pos; intros; apply pos_INR.
-  replace (2 * N - k - N)%nat with (N - k)%nat.
-  rewrite Rmult_comm; rewrite (prod_SO_split (fun l:nat => INR l) N k).
+  apply prod_SO_pos; intros; auto.
+  replace (2 * N - k - N-1)%nat with (N - k-1)%nat.
+  rewrite Rmult_comm; rewrite (prod_SO_split 
+        (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) N k).
   apply Rmult_le_compat_l.
-  apply prod_SO_pos; intros; apply pos_INR.
-  apply prod_SO_Rle; intros; split.
-  apply pos_INR.
-  apply le_INR; apply plus_le_compat_r; assumption.
+  apply prod_SO_pos; intros; auto.
+  apply prod_SO_Rle; intros; split; auto.
+  rewrite H0.
+  rewrite H0.
+  apply le_INR; omega.
+  omega.
+  omega.
   assumption.
   omega.
   omega.
-  rewrite <- (Rmult_comm (prod_f_SO (fun l:nat => INR l) k));
-    rewrite (prod_SO_split (fun l:nat => INR l) k N).
+  rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat => 
+          if eq_nat_dec l 0 then 1 else INR l) k));
+    rewrite (prod_SO_split (fun l:nat => 
+          if eq_nat_dec l 0 then 1 else INR l) k N).
   rewrite Rmult_assoc; apply Rmult_le_compat_l.
-  apply prod_SO_pos; intros; apply pos_INR.
+  apply prod_SO_pos; intros; auto.
   rewrite Rmult_comm;
-    rewrite (prod_SO_split (fun l:nat => INR l) N (2 * N - k)).
+    rewrite (prod_SO_split (fun l:nat => 
+          if eq_nat_dec l 0 then 1 else INR l) N (2 * N - k)).
   apply Rmult_le_compat_l.
-  apply prod_SO_pos; intros; apply pos_INR.
-  replace (N - (2 * N - k))%nat with (k - N)%nat.
-  apply prod_SO_Rle; intros; split.
-  apply pos_INR.
-  apply le_INR; apply plus_le_compat_r.
+  apply prod_SO_pos; intros; auto.
+  replace (N - (2 * N - k)-1)%nat with (k - N-1)%nat.
+  apply prod_SO_Rle; intros; split; auto.
+  rewrite H0.
+  rewrite H0.
+  apply le_INR; omega.
+  omega.
   omega.
   omega.
   omega.
   assumption.
   omega.
-Qed.
+Qed. 
+
 
 (**********)
 Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n).
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 38c39bae..702aafa4 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rseries.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rseries.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -194,14 +194,14 @@ Section Isequence.
   Variable An : nat -> R.
 
 (*********)
-  Definition Pser (x l:R) : Prop := infinit_sum (fun n:nat => An n * x ^ n) l.
+  Definition Pser (x l:R) : Prop := infinite_sum (fun n:nat => An n * x ^ n) l.
 
 End Isequence.
 
 Lemma GP_infinite :
   forall x:R, Rabs x < 1 -> Pser (fun n:nat => 1) x (/ (1 - x)).
 Proof.
-  intros; unfold Pser in |- *; unfold infinit_sum in |- *; intros;
+  intros; unfold Pser in |- *; unfold infinite_sum in |- *; intros;
     elim (Req_dec x 0).
   intros; exists 0%nat; intros; rewrite H1; rewrite Rminus_0_r; rewrite Rinv_1;
     cut (sum_f_R0 (fun n0:nat => 1 * 0 ^ n0) n = 1).
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index cb31d3b2..7cdd4d02 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsigma.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rsigma.v 9454 2006-12-15 15:30:59Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 0a9f7754..0a3af6ca 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsqrt_def.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rsqrt_def.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Sumbool.
 Require Import Rbase.
@@ -192,7 +192,7 @@ Qed.
 
 Lemma dicho_lb_cv :
   forall (x y:R) (P:R -> bool),
-    x <= y -> sigT (fun l:R => Un_cv (dicho_lb x y P) l).
+    x <= y -> { l:R | Un_cv (dicho_lb x y P) l }.
 Proof.
   intros.
   apply growing_cv.
@@ -202,7 +202,7 @@ Qed.
 
 Lemma dicho_up_cv :
   forall (x y:R) (P:R -> bool),
-    x <= y -> sigT (fun l:R => Un_cv (dicho_up x y P) l).
+    x <= y -> { l:R | Un_cv (dicho_up x y P) l }.
 Proof.
   intros.
   apply decreasing_cv.
@@ -466,7 +466,7 @@ Qed.
 Lemma IVT :
   forall (f:R -> R) (x y:R),
     continuity f ->
-    x < y -> f x < 0 -> 0 < f y -> sigT (fun z:R => x <= z <= y /\ f z = 0).
+    x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }.
 Proof.
   intros.
   cut (x <= y).
@@ -478,7 +478,7 @@ Proof.
   elim X0; intros.
   assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
   rewrite H4 in p0.
-  apply existT with x0.
+  exists x0.
   split.
   split.
   apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0).
@@ -602,7 +602,7 @@ Qed.
 Lemma IVT_cor :
   forall (f:R -> R) (x y:R),
     continuity f ->
-    x <= y -> f x * f y <= 0 -> sigT (fun z:R => x <= z <= y /\ f z = 0).
+    x <= y -> f x * f y <= 0 -> { z:R | x <= z <= y /\ f z = 0 }.
 Proof.
   intros.
   case (total_order_T 0 (f x)); intro.
@@ -628,7 +628,7 @@ Proof.
   cut (0 < (- f)%F y).
   intros.
   elim (H3 H5 H4); intros.
-  apply existT with x0.
+  exists x0.
   elim p; intros.
   split.
   assumption.
@@ -643,7 +643,7 @@ Proof.
   assumption.
   rewrite H2 in a.
   elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
-  apply existT with x.
+  exists x.
   split.
   split; [ right; reflexivity | assumption ].
   symmetry  in |- *; assumption.
@@ -656,7 +656,7 @@ Proof.
   assumption.
   rewrite H2 in r.
   elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
-  apply existT with y.
+  exists y.
   split.
   split; [ assumption | right; reflexivity ].
   symmetry  in |- *; assumption.
@@ -670,7 +670,7 @@ Qed.
 (** We can now define the square root function as the reciprocal 
    transformation of the square root function *)
 Lemma Rsqrt_exists :
-  forall y:R, 0 <= y -> sigT (fun z:R => 0 <= z /\ y = Rsqr z).
+  forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }.
 Proof.
   intros.
   set (f := fun x:R => Rsqr x - y).
@@ -686,7 +686,7 @@ Proof.
   intro.
   assert (X := IVT_cor f 0 1 H1 (Rlt_le _ _ Rlt_0_1) H3).
   elim X; intros t H4.
-  apply existT with t.
+  exists t.
   elim H4; intros.
   split.
   elim H5; intros; assumption.
@@ -700,7 +700,7 @@ Proof.
   rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *;
     rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; 
       left; assumption.
-  apply existT with 1.
+  exists 1.
   split.
   left; apply Rlt_0_1.
   rewrite b; symmetry  in |- *; apply Rsqr_1.
@@ -710,7 +710,7 @@ Proof.
   intro.
   assert (X := IVT_cor f 0 y H1 H H3).
   elim X; intros t H4.
-  apply existT with t.
+  exists t.
   elim H4; intros.
   split.
   elim H5; intros; assumption.
@@ -739,9 +739,7 @@ Qed.
 
 (* Definition of the square root: R+->R *)
 Definition Rsqrt (y:nonnegreal) : R :=
-  match Rsqrt_exists (nonneg y) (cond_nonneg y) with
-    | existT a b => a
-  end.
+  let (a,_) := Rsqrt_exists (nonneg y) (cond_nonneg y) in a.
 
 (**********)
 Lemma Rsqrt_positivity : forall x:nonnegreal, 0 <= Rsqrt x.
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index aa47d72f..9501bc1e 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -6,15 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtopology.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtopology.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
 Require Import RList.
 Require Import Classical_Prop.
-Require Import Classical_Pred_Type. Open Local Scope R_scope.
-
+Require Import Classical_Pred_Type.
+Open Local Scope R_scope.
 
 (** * General definitions and propositions *)
 
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index b744c788..0baece39 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rtrigo.v 9454 2006-12-15 15:30:59Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 89ee1745..d82bafc6 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_alt.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rtrigo_alt.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -137,7 +137,7 @@ Proof.
   ring.
   assert (X := exist_sin (Rsqr a)); elim X; intros.
   cut (x = sin a / a).
-  intro; rewrite H3 in p; unfold sin_in in p; unfold infinit_sum in p;
+  intro; rewrite H3 in p; unfold sin_in in p; unfold infinite_sum in p;
     unfold R_dist in p; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros.
   cut (0 < eps / Rabs a).
@@ -327,7 +327,7 @@ Proof.
   apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_S; assumption.
   assert (X := exist_cos (Rsqr a0)); elim X; intros.
   cut (x = cos a0).
-  intro; rewrite H4 in p; unfold cos_in in p; unfold infinit_sum in p;
+  intro; rewrite H4 in p; unfold cos_in in p; unfold infinite_sum in p;
     unfold R_dist in p; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros.
   elim (p _ H5); intros N H6.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index b2aeb766..e94d7448 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_def.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo_def.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -19,7 +19,7 @@ Open Local Scope R_scope.
 (** * Definition of exponential *)
 (********************************)
 Definition exp_in (x l:R) : Prop :=
-  infinit_sum (fun i:nat => / INR (fact i) * x ^ i) l.
+  infinite_sum (fun i:nat => / INR (fact i) * x ^ i) l.
 
 Lemma exp_cof_no_R0 : forall n:nat, / INR (fact n) <> 0.
 Proof.
@@ -28,7 +28,7 @@ Proof.
   apply INR_fact_neq_0.
 Qed.
 
-Lemma exist_exp : forall x:R, sigT (fun l:R => exp_in x l).
+Lemma exist_exp : forall x:R, { l:R | exp_in x l }.
 Proof.
   intro;
     generalize
@@ -37,7 +37,7 @@ Proof.
   trivial.
 Defined.
 
-Definition exp (x:R) : R := projT1 (exist_exp x).
+Definition exp (x:R) : R := proj1_sig (exist_exp x).
 
 Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0.
 Proof.
@@ -45,11 +45,10 @@ Proof.
   red in |- *; intro; rewrite H0 in H; elim (lt_irrefl _ H).
 Qed.
 
-(*i Calculus of $e^0$ *)
-Lemma exist_exp0 : sigT (fun l:R => exp_in 0 l).
+Lemma exist_exp0 : { l:R | exp_in 0 l }.
 Proof.
-  apply existT with 1.
-  unfold exp_in in |- *; unfold infinit_sum in |- *; intros.
+  exists 1.
+  unfold exp_in in |- *; unfold infinite_sum in |- *; intros.
   exists 0%nat.
   intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1.
   unfold R_dist in |- *; replace (1 - 1) with 0;
@@ -63,6 +62,7 @@ Proof.
   unfold ge in |- *; apply le_O_n.
 Defined.
 
+(* Value of [exp 0] *)
 Lemma exp_0 : exp 0 = 1. 
 Proof.
   cut (exp_in 0 (exp 0)).
@@ -70,8 +70,8 @@ Proof.
   unfold exp_in in |- *; intros; eapply uniqueness_sum.
   apply H0.
   apply H.
-  exact (projT2 exist_exp0).
-  exact (projT2 (exist_exp 0)).
+  exact (proj2_sig exist_exp0).
+  exact (proj2_sig (exist_exp 0)).
 Qed.
 
 (*****************************************)
@@ -235,21 +235,17 @@ Qed.
 
 (**********)
 Definition cos_in (x l:R) : Prop :=
-  infinit_sum (fun i:nat => cos_n i * x ^ i) l.
+  infinite_sum (fun i:nat => cos_n i * x ^ i) l.
 
 (**********)
-Lemma exist_cos : forall x:R, sigT (fun l:R => cos_in x l).
+Lemma exist_cos : forall x:R, { l:R | cos_in x l }.
   intro; generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos).
   unfold Pser, cos_in in |- *; trivial.
 Qed.
 
 
 (** Definition of cosinus *)
-Definition cos (x:R) : R :=
-  match exist_cos (Rsqr x) with
-    | existT a b => a
-  end.
-
+Definition cos (x:R) : R := let (a,_) := exist_cos (Rsqr x) in a.
 
 Definition sin_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n + 1)).
 
@@ -348,7 +344,7 @@ Proof.
   apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR;
     rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR;
       replace (INR 0) with 0; [ ring | reflexivity ].
-Qed.
+Defined.
 
 Lemma sin_no_R0 : forall n:nat, sin_n n <> 0.
 Proof.
@@ -359,21 +355,18 @@ Qed.
 
 (**********)
 Definition sin_in (x l:R) : Prop :=
-  infinit_sum (fun i:nat => sin_n i * x ^ i) l.
+  infinite_sum (fun i:nat => sin_n i * x ^ i) l.
 
 (**********)
-Lemma exist_sin : forall x:R, sigT (fun l:R => sin_in x l).
+Lemma exist_sin : forall x:R, { l:R | sin_in x l }.
 Proof.
   intro; generalize (Alembert_C3 sin_n x sin_no_R0 Alembert_sin).
   unfold Pser, sin_n in |- *; trivial.
-Qed.
+Defined.
 
 (***********************)
 (* Definition of sinus *)
-Definition sin (x:R) : R :=
-  match exist_sin (Rsqr x) with
-    | existT a b => x * a
-  end.
+Definition sin (x:R) : R := let (a,_) := exist_sin (Rsqr x) in x * a.
 
 (*********************************************)
 (** *              Properties                *)
@@ -399,10 +392,10 @@ Proof.
   intros; ring.
 Qed.
 
-Lemma exist_cos0 : sigT (fun l:R => cos_in 0 l).
+Lemma exist_cos0 : { l:R | cos_in 0 l }.
 Proof.
-  apply existT with 1.
-  unfold cos_in in |- *; unfold infinit_sum in |- *; intros; exists 0%nat.
+  exists 1.
+  unfold cos_in in |- *; unfold infinite_sum in |- *; intros; exists 0%nat.
   intros.
   unfold R_dist in |- *.
   induction  n as [| n Hrecn].
@@ -417,7 +410,7 @@ Proof.
   simpl in |- *; ring.
 Defined.
 
-(* Calculus of (cos 0) *)
+(* Value of [cos 0] *)
 Lemma cos_0 : cos 0 = 1.
 Proof.
   cut (cos_in 0 (cos 0)).
@@ -425,7 +418,7 @@ Proof.
   unfold cos_in in |- *; intros; eapply uniqueness_sum.
   apply H0.
   apply H.
-  exact (projT2 exist_cos0).
-  assert (H := projT2 (exist_cos (Rsqr 0))); unfold cos in |- *;
+  exact (proj2_sig exist_cos0).
+  assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos in |- *;
     pattern 0 at 1 in |- *; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ].
 Qed.
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index 78ef847f..6eec0329 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_fun.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo_fun.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -15,8 +15,7 @@ Open Local Scope R_scope.
 
 (*****************************************************************)
 (**           To define transcendental functions                 *)
-(**           for exponential function                           *)
-(*                                                               *)
+(**           and exponential function                           *)
 (*****************************************************************)
 
 (*********)
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index b105ca69..139563bf 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_reg.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rtrigo_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -25,16 +25,15 @@ Proof.
   unfold CVN_R in |- *; intros.
   cut ((r:R) <> 0).
   intro hyp_r; unfold CVN_r in |- *.
-  apply existT with (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)).
+  exists (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)).
   cut
-    (sigT
-      (fun l:R =>
+    { l:R |
         Un_cv
         (fun n:nat =>
           sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k)))
-          n) l)).
+          n) l }.
   intro X; elim X; intros.
-  apply existT with x.
+  exists x.
   split.
   apply p.
   intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult.
@@ -124,7 +123,7 @@ Lemma continuity_cos : continuity cos.
 Proof.
   set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)).
   cut (CVN_R fn).
-  intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)).
+  intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }).
   intro cv; cut (forall n:nat, continuity (fn n)).
   intro; cut (forall x:R, cos x = SFL fn cv x).
   intro; cut (continuity (SFL fn cv) -> continuity cos).
@@ -144,7 +143,7 @@ Proof.
   case (cv x); case (exist_cos (Rsqr x)); intros.
   symmetry  in |- *; eapply UL_sequence.
   apply u.
-  unfold cos_in in c; unfold infinit_sum in c; unfold Un_cv in |- *; intros.
+  unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros.
   elim (c _ H0); intros N0 H1.
   exists N0; intros.
   unfold R_dist in H1; unfold R_dist, SP in |- *.
@@ -200,17 +199,16 @@ Lemma CVN_R_sin :
     CVN_R fn.
 Proof.
   unfold CVN_R in |- *; unfold CVN_r in |- *; intros fn H r.
-  apply existT with (fun n:nat => / INR (fact (2 * n + 1)) * r ^ (2 * n)).
+  exists (fun n:nat => / INR (fact (2 * n + 1)) * r ^ (2 * n)).
   cut
-    (sigT
-      (fun l:R =>
+    { l:R |
         Un_cv
         (fun n:nat =>
           sum_f_R0
           (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n)
-        l)).
+        l }.
   intro X; elim X; intros.
-  apply existT with x.
+  exists x.
   split.
   apply p.
   intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult;
@@ -305,7 +303,7 @@ Proof.
   set
     (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)).
   cut (CVN_R fn).
-  intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)).
+  intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }).
   intro cv.
   set (r := mkposreal _ Rlt_0_1).
   cut (CVN_r fn r).
@@ -331,7 +329,7 @@ Proof.
   unfold Rdiv in |- *; rewrite (Rinv_r_simpl_m h x0 H6).
   eapply UL_sequence.
   apply u.
-  unfold sin_in in s; unfold sin_n, infinit_sum in s;
+  unfold sin_in in s; unfold sin_n, infinite_sum in s;
     unfold SP, fn, Un_cv in |- *; intros.
   elim (s _ H10); intros N0 H11.
   exists N0; intros.
@@ -584,14 +582,14 @@ Qed.
 Lemma derivable_pt_sin : forall x:R, derivable_pt sin x.
 Proof.
   unfold derivable_pt in |- *; intro.
-  apply existT with (cos x).
+  exists (cos x).
   apply derivable_pt_lim_sin.
 Qed.
 
 Lemma derivable_pt_cos : forall x:R, derivable_pt cos x.
 Proof.
   unfold derivable_pt in |- *; intro.
-  apply existT with (- sin x).
+  exists (- sin x).
   apply derivable_pt_lim_cos.
 Qed.
 
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 96351618..56088a2e 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: SeqProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: SeqProp.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -15,6 +15,10 @@ Require Import Classical.
 Require Import Max.
 Open Local Scope R_scope.
 
+(*****************************************************************)
+(**           Convergence properties of sequences                *)
+(*****************************************************************)
+
 Definition Un_decreasing (Un:nat -> R) : Prop :=
   forall n:nat, Un (S n) <= Un n.
 Definition opp_seq (Un:nat -> R) (n:nat) : R := - Un n.
@@ -23,8 +27,7 @@ Definition has_lb (Un:nat -> R) : Prop := bound (EUn (opp_seq Un)).
 
 (**********)
 Lemma growing_cv :
-  forall Un:nat -> R,
-    Un_growing Un -> has_ub Un -> sigT (fun l:R => Un_cv Un l).
+  forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l:R | Un_cv Un l }.
 Proof.
   unfold Un_growing, Un_cv in |- *; intros;
     destruct (completeness (EUn Un) H0 (EUn_noempty Un)) as [x [H2 H3]].
@@ -64,11 +67,10 @@ Proof.
 Qed.
 
 Lemma decreasing_cv :
-  forall Un:nat -> R,
-    Un_decreasing Un -> has_lb Un -> sigT (fun l:R => Un_cv Un l).
+  forall Un:nat -> R, Un_decreasing Un -> has_lb Un -> { l:R | Un_cv Un l }.
 Proof.
   intros.
-  cut (sigT (fun l:R => Un_cv (opp_seq Un) l) -> sigT (fun l:R => Un_cv Un l)).
+  cut ({ l:R | Un_cv (opp_seq Un) l } -> { l:R | Un_cv Un l }).
   intro X.
   apply X.
   apply growing_cv.
@@ -76,7 +78,7 @@ Proof.
   exact H0.
   intro X.
   elim X; intros.
-  apply existT with (- x).
+  exists (- x).
   unfold Un_cv in p.
   unfold R_dist in p.
   unfold opp_seq in p.
@@ -91,8 +93,8 @@ Proof.
 Qed.
 
 (***********)
-Lemma maj_sup :
-  forall Un:nat -> R, has_ub Un -> sigT (fun l:R => is_lub (EUn Un) l).
+Lemma ub_to_lub :
+  forall Un:nat -> R, has_ub Un -> { l:R | is_lub (EUn Un) l }.
 Proof.
   intros.
   unfold has_ub in H.
@@ -104,9 +106,8 @@ Proof.
 Qed.
 
 (**********)
-Lemma min_inf :
-  forall Un:nat -> R,
-    has_lb Un -> sigT (fun l:R => is_lub (EUn (opp_seq Un)) l).
+Lemma lb_to_glb :
+  forall Un:nat -> R, has_lb Un -> { l:R | is_lub (EUn (opp_seq Un)) l }.
 Proof.
   intros; unfold has_lb in H.
   apply completeness.
@@ -116,15 +117,17 @@ Proof.
   reflexivity.
 Qed.
 
-Definition majorant (Un:nat -> R) (pr:has_ub Un) : R :=
-  match maj_sup Un pr with
-    | existT a b => a
-  end.
+Definition lub (Un:nat -> R) (pr:has_ub Un) : R :=
+  let (a,_) := ub_to_lub Un pr in a.
 
-Definition minorant (Un:nat -> R) (pr:has_lb Un) : R :=
-  match min_inf Un pr with
-    | existT a b => - a
-  end.
+Definition glb (Un:nat -> R) (pr:has_lb Un) : R :=
+  let (a,_) := lb_to_glb Un pr in - a.
+
+(* Compatibility with previous unappropriate terminology *)
+Notation maj_sup := ub_to_lub (only parsing).
+Notation min_inf := lb_to_glb (only parsing).
+Notation majorant := lub (only parsing).
+Notation minorant := glb (only parsing).
 
 Lemma maj_ss :
   forall (Un:nat -> R) (k:nat),
@@ -162,26 +165,30 @@ Proof.
   exists (k + x1)%nat; assumption.
 Qed.
 
-Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un)
-  (i:nat) : R := majorant (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr).
+Definition sequence_ub (Un:nat -> R) (pr:has_ub Un)
+  (i:nat) : R := lub (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr).
+
+Definition sequence_lb (Un:nat -> R) (pr:has_lb Un)
+  (i:nat) : R := glb (fun k:nat => Un (i + k)%nat) (min_ss Un i pr).
 
-Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un)
-  (i:nat) : R := minorant (fun k:nat => Un (i + k)%nat) (min_ss Un i pr).
+(* Compatibility *)
+Notation sequence_majorant := sequence_ub (only parsing).
+Notation sequence_minorant := sequence_lb (only parsing).
 
 Lemma Wn_decreasing :
-  forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr).
+  forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr).
 Proof.
   intros.
   unfold Un_decreasing in |- *.
   intro.
-  unfold sequence_majorant in |- *.
-  assert (H := maj_sup (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
-  assert (H0 := maj_sup (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
+  unfold sequence_ub in |- *.
+  assert (H := ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
+  assert (H0 := ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
   elim H; intros.
   elim H0; intros.
-  cut (majorant (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x);
+  cut (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x);
     [ intro Maj1; rewrite Maj1 | idtac ].
-  cut (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr) = x0);
+  cut (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr) = x0);
     [ intro Maj2; rewrite Maj2 | idtac ].
   unfold is_lub in p.
   unfold is_lub in p0.
@@ -199,47 +206,47 @@ Proof.
   replace (S n) with (1 + n)%nat; [ ring | ring ].
   cut
     (is_lub (EUn (fun k:nat => Un (n + k)%nat))
-      (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr))).
+      (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr))).
   intro.
   unfold is_lub in p0; unfold is_lub in H1.
   elim p0; intros; elim H1; intros.
   assert (H6 := H5 x0 H2).
   assert
-    (H7 := H3 (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H4).
+    (H7 := H3 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H4).
   apply Rle_antisym; assumption.
-  unfold majorant in |- *.
-  case (maj_sup (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
+  unfold lub in |- *.
+  case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
   trivial.
   cut
     (is_lub (EUn (fun k:nat => Un (S n + k)%nat))
-      (majorant (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr))).
+      (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr))).
   intro.
   unfold is_lub in p; unfold is_lub in H1.
   elim p; intros; elim H1; intros.
   assert (H6 := H5 x H2).
   assert
     (H7 :=
-      H3 (majorant (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H4).
+      H3 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H4).
   apply Rle_antisym; assumption.
-  unfold majorant in |- *.
-  case (maj_sup (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
+  unfold lub in |- *.
+  case (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
   trivial.
 Qed.
 
 Lemma Vn_growing :
-  forall (Un:nat -> R) (pr:has_lb Un), Un_growing (sequence_minorant Un pr).
+  forall (Un:nat -> R) (pr:has_lb Un), Un_growing (sequence_lb Un pr).
 Proof.
   intros.
   unfold Un_growing in |- *.
   intro.
-  unfold sequence_minorant in |- *.
-  assert (H := min_inf (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)).
-  assert (H0 := min_inf (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)).
+  unfold sequence_lb in |- *.
+  assert (H := lb_to_glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)).
+  assert (H0 := lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)).
   elim H; intros.
   elim H0; intros.
-  cut (minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr) = - x);
+  cut (glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr) = - x);
     [ intro Maj1; rewrite Maj1 | idtac ].
-  cut (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr) = - x0);
+  cut (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr) = - x0);
     [ intro Maj2; rewrite Maj2 | idtac ].
   unfold is_lub in p.
   unfold is_lub in p0.
@@ -260,38 +267,38 @@ Proof.
   replace (S n) with (1 + n)%nat; [ ring | ring ].
   cut
     (is_lub (EUn (opp_seq (fun k:nat => Un (n + k)%nat)))
-      (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))).
+      (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))).
   intro.
   unfold is_lub in p0; unfold is_lub in H1.
   elim p0; intros; elim H1; intros.
   assert (H6 := H5 x0 H2).
   assert
-    (H7 := H3 (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)) H4).
+    (H7 := H3 (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)) H4).
   rewrite <-
-    (Ropp_involutive (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)))
+    (Ropp_involutive (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)))
     .
   apply Ropp_eq_compat; apply Rle_antisym; assumption.
-  unfold minorant in |- *.
-  case (min_inf (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)).
+  unfold glb in |- *.
+  case (lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)); simpl.
   intro; rewrite Ropp_involutive.
   trivial.
   cut
     (is_lub (EUn (opp_seq (fun k:nat => Un (S n + k)%nat)))
-      (- minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))).
+      (- glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))).
   intro.
   unfold is_lub in p; unfold is_lub in H1.
   elim p; intros; elim H1; intros.
   assert (H6 := H5 x H2).
   assert
     (H7 :=
-      H3 (- minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)) H4).
+      H3 (- glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)) H4).
   rewrite <-
     (Ropp_involutive
-      (minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)))
+      (glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)))
     .
   apply Ropp_eq_compat; apply Rle_antisym; assumption.
-  unfold minorant in |- *.
-  case (min_inf (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)).
+  unfold glb in |- *.
+  case (lb_to_glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)); simpl.
   intro; rewrite Ropp_involutive.
   trivial.
 Qed.
@@ -299,16 +306,15 @@ Qed.
 (**********)
 Lemma Vn_Un_Wn_order :
   forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un)
-    (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n.
+    (n:nat), sequence_lb Un pr2 n <= Un n <= sequence_ub Un pr1 n.
 Proof.
   intros.
   split.
-  unfold sequence_minorant in |- *.
-  cut
-    (sigT (fun l:R => is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l)).
+  unfold sequence_lb in |- *.
+  cut { l:R | is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l }.
   intro X.
   elim X; intros.
-  replace (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x).
+  replace (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x).
   unfold is_lub in p.
   elim p; intros.
   unfold is_upper_bound in H.
@@ -320,28 +326,28 @@ Proof.
   replace (n + 0)%nat with n; [ reflexivity | ring ].
   cut
     (is_lub (EUn (opp_seq (fun k:nat => Un (n + k)%nat)))
-      (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2))).
+      (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2))).
   intro.
   unfold is_lub in p; unfold is_lub in H.
   elim p; intros; elim H; intros.
   assert (H4 := H3 x H0).
   assert
-    (H5 := H1 (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) H2).
+    (H5 := H1 (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) H2).
   rewrite <-
-    (Ropp_involutive (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)))
+    (Ropp_involutive (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)))
     .
   apply Ropp_eq_compat; apply Rle_antisym; assumption.
-  unfold minorant in |- *.
-  case (min_inf (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)).
+  unfold glb in |- *.
+  case (lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)); simpl.
   intro; rewrite Ropp_involutive.
   trivial.
-  apply min_inf.
+  apply lb_to_glb.
   apply min_ss; assumption.
-  unfold sequence_majorant in |- *.
-  cut (sigT (fun l:R => is_lub (EUn (fun i:nat => Un (n + i)%nat)) l)).
+  unfold sequence_ub in |- *.
+  cut { l:R | is_lub (EUn (fun i:nat => Un (n + i)%nat)) l }.
   intro X.
   elim X; intros.
-  replace (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x.
+  replace (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x.
   unfold is_lub in p.
   elim p; intros.
   unfold is_upper_bound in H.
@@ -350,24 +356,24 @@ Proof.
   replace (n + 0)%nat with n; [ reflexivity | ring ].
   cut
     (is_lub (EUn (fun k:nat => Un (n + k)%nat))
-      (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1))).
+      (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1))).
   intro.
   unfold is_lub in p; unfold is_lub in H.
   elim p; intros; elim H; intros.
   assert (H4 := H3 x H0).
   assert
-    (H5 := H1 (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) H2).
+    (H5 := H1 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) H2).
   apply Rle_antisym; assumption.
-  unfold majorant in |- *.
-  case (maj_sup (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)).
+  unfold lub in |- *.
+  case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)).
   intro; trivial.
-  apply maj_sup.
+  apply ub_to_lub.
   apply maj_ss; assumption.
 Qed.
 
 Lemma min_maj :
   forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un),
-    has_ub (sequence_minorant Un pr2).
+    has_ub (sequence_lb Un pr2).
 Proof.
   intros.
   assert (H := Vn_Un_Wn_order Un pr1 pr2).
@@ -390,7 +396,7 @@ Qed.
 
 Lemma maj_min :
   forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un),
-    has_lb (sequence_majorant Un pr1).
+    has_lb (sequence_ub Un pr1).
 Proof.
   intros.
   assert (H := Vn_Un_Wn_order Un pr1 pr2).
@@ -451,7 +457,7 @@ Qed.
 (**********)
 Lemma maj_cv :
   forall (Un:nat -> R) (pr:Cauchy_crit Un),
-    sigT (fun l:R => Un_cv (sequence_majorant Un (cauchy_maj Un pr)) l).
+    { l:R | Un_cv (sequence_ub Un (cauchy_maj Un pr)) l }.
 Proof.
   intros.
   apply decreasing_cv.
@@ -464,7 +470,7 @@ Qed.
 (**********)
 Lemma min_cv :
   forall (Un:nat -> R) (pr:Cauchy_crit Un),
-    sigT (fun l:R => Un_cv (sequence_minorant Un (cauchy_min Un pr)) l).
+    { l:R | Un_cv (sequence_lb Un (cauchy_min Un pr)) l }.
 Proof.
   intros.
   apply growing_cv.
@@ -510,40 +516,40 @@ 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 (lub Un pr - Un k) < eps.
 Proof.
   intros.
-  set (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps).
+  set (P := fun k:nat => Rabs (lub 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, Rabs (lub Un pr - Un k) < eps).
   intros.
   apply H0.
   apply not_all_not_ex.
   red in |- *; intro.
   2: unfold P in |- *; trivial.
   unfold P in H1.
-  cut (forall n:nat, Rabs (majorant Un pr - Un n) >= eps).
+  cut (forall n:nat, Rabs (lub Un pr - Un n) >= eps).
   intro.
-  cut (is_lub (EUn Un) (majorant Un pr)).
+  cut (is_lub (EUn Un) (lub Un pr)).
   intro.
   unfold is_lub in H3.
   unfold is_upper_bound in H3.
   elim H3; intros.
-  cut (forall n:nat, eps <= majorant Un pr - Un n).
+  cut (forall n:nat, eps <= lub Un pr - Un n).
   intro.
-  cut (forall n:nat, Un n <= majorant Un pr - eps).
+  cut (forall n:nat, Un n <= lub Un pr - eps).
   intro.
-  cut (forall x:R, EUn Un x -> x <= majorant Un pr - eps).
+  cut (forall x:R, EUn Un x -> x <= lub Un pr - eps).
   intro.
-  assert (H9 := H5 (majorant Un pr - eps) H8).
+  assert (H9 := H5 (lub Un pr - eps) H8).
   cut (eps <= 0).
   intro.
   elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H H10)).
-  apply Rplus_le_reg_l with (majorant Un pr - eps).
+  apply Rplus_le_reg_l with (lub Un pr - eps).
   rewrite Rplus_0_r.
-  replace (majorant Un pr - eps + eps) with (majorant Un pr);
+  replace (lub Un pr - eps + eps) with (lub Un pr);
   [ assumption | ring ].
   intros.
   unfold EUn in H8.
@@ -553,7 +559,7 @@ Proof.
   assert (H7 := H6 n).
   apply Rplus_le_reg_l with (eps - Un n).
   replace (eps - Un n + Un n) with eps.
-  replace (eps - Un n + (majorant Un pr - eps)) with (majorant Un pr - Un n).
+  replace (eps - Un n + (lub Un pr - eps)) with (lub Un pr - Un n).
   assumption.
   ring.
   ring.
@@ -565,11 +571,11 @@ Proof.
   apply Rle_ge.
   apply Rplus_le_reg_l with (Un n).
   rewrite Rplus_0_r;
-    replace (Un n + (majorant Un pr - Un n)) with (majorant Un pr);
+    replace (Un n + (lub Un pr - Un n)) with (lub Un pr);
     [ apply H4 | ring ].
   exists n; reflexivity.
-  unfold majorant in |- *.
-  case (maj_sup Un pr).
+  unfold lub in |- *.
+  case (ub_to_lub Un pr).
   trivial.
   intro.
   assert (H2 := H1 n).
@@ -579,40 +585,40 @@ 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 (glb Un pr - Un k) < eps.
 Proof.
   intros.
-  set (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps).
+  set (P := fun k:nat => Rabs (glb 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, Rabs (glb Un pr - Un k) < eps).
   intros.
   apply H0.
   apply not_all_not_ex.
   red in |- *; intro.
   2: unfold P in |- *; trivial.
   unfold P in H1.
-  cut (forall n:nat, Rabs (minorant Un pr - Un n) >= eps).
+  cut (forall n:nat, Rabs (glb Un pr - Un n) >= eps).
   intro.
-  cut (is_lub (EUn (opp_seq Un)) (- minorant Un pr)).
+  cut (is_lub (EUn (opp_seq Un)) (- glb Un pr)).
   intro.
   unfold is_lub in H3.
   unfold is_upper_bound in H3.
   elim H3; intros.
-  cut (forall n:nat, eps <= Un n - minorant Un pr).
+  cut (forall n:nat, eps <= Un n - glb Un pr).
   intro.
-  cut (forall n:nat, opp_seq Un n <= - minorant Un pr - eps).
+  cut (forall n:nat, opp_seq Un n <= - glb Un pr - eps).
   intro.
-  cut (forall x:R, EUn (opp_seq Un) x -> x <= - minorant Un pr - eps).
+  cut (forall x:R, EUn (opp_seq Un) x -> x <= - glb Un pr - eps).
   intro.
-  assert (H9 := H5 (- minorant Un pr - eps) H8).
+  assert (H9 := H5 (- glb Un pr - eps) H8).
   cut (eps <= 0).
   intro.
   elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H H10)).
-  apply Rplus_le_reg_l with (- minorant Un pr - eps).
+  apply Rplus_le_reg_l with (- glb Un pr - eps).
   rewrite Rplus_0_r.
-  replace (- minorant Un pr - eps + eps) with (- minorant Un pr);
+  replace (- glb Un pr - eps + eps) with (- glb Un pr);
   [ assumption | ring ].
   intros.
   unfold EUn in H8.
@@ -623,7 +629,7 @@ Proof.
   unfold opp_seq in |- *.
   apply Rplus_le_reg_l with (eps + Un n).
   replace (eps + Un n + - Un n) with eps.
-  replace (eps + Un n + (- minorant Un pr - eps)) with (Un n - minorant Un pr).
+  replace (eps + Un n + (- glb Un pr - eps)) with (Un n - glb Un pr).
   assumption.
   ring.
   ring.
@@ -631,16 +637,16 @@ Proof.
   assert (H6 := H2 n).
   rewrite Rabs_left1 in H6.
   apply Rge_le.
-  replace (Un n - minorant Un pr) with (- (minorant Un pr - Un n));
+  replace (Un n - glb Un pr) with (- (glb Un pr - Un n));
   [ assumption | ring ].
-  apply Rplus_le_reg_l with (- minorant Un pr).
+  apply Rplus_le_reg_l with (- glb Un pr).
   rewrite Rplus_0_r;
-    replace (- minorant Un pr + (minorant Un pr - Un n)) with (- Un n).
+    replace (- glb Un pr + (glb Un pr - Un n)) with (- Un n).
   apply H4.
   exists n; reflexivity.
   ring.
-  unfold minorant in |- *.
-  case (min_inf Un pr).
+  unfold glb in |- *.
+  case (lb_to_glb Un pr); simpl.
   intro.
   rewrite Ropp_involutive.
   trivial.
@@ -711,7 +717,7 @@ Qed.
 
 (**********)
 Lemma CV_Cauchy :
-  forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un.
+  forall Un:nat -> R, { l:R | Un_cv Un l } -> Cauchy_crit Un.
 Proof.
   intros Un X; elim X; intros.
   unfold Cauchy_crit in |- *; intros.
@@ -734,11 +740,11 @@ Qed.
 (**********)
 Lemma maj_by_pos :
   forall Un:nat -> R,
-    sigT (fun l:R => Un_cv Un l) ->
+    { l:R | Un_cv Un l } ->
     exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l).
 Proof.
   intros Un X; elim X; intros.
-  cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)).
+  cut { l:R | Un_cv (fun k:nat => Rabs (Un k)) l }.
   intro X0.
   assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0).
   assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H).
@@ -760,7 +766,7 @@ Proof.
   unfold is_upper_bound in H1.
   apply H1.
   exists 0%nat; reflexivity.
-  apply existT with (Rabs x).
+  exists (Rabs x).
   apply cv_cvabs; assumption.
 Qed.
 
@@ -770,7 +776,7 @@ Lemma CV_mult :
     Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2).
 Proof.
   intros.
-  cut (sigT (fun l:R => Un_cv An l)).
+  cut { l:R | Un_cv An l }.
   intro X.
   assert (H1 := maj_by_pos An X).
   elim H1; intros M H2.
@@ -881,7 +887,7 @@ Proof.
     [ assumption
       | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat;
         [ prove_sup0 | assumption ] ].
-  apply existT with l1; assumption.
+  exists l1; assumption.
 Qed.
 
 Lemma tech9 :
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index bc17cd43..9680b75e 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: SeqSeries.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: SeqSeries.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -33,15 +33,9 @@ Lemma sum_maj1 :
     Rabs (l1 - SP fn N x) <= l2 - sum_f_R0 An N.
 Proof.
   intros;
-    cut
-      (sigT
-        (fun l:R =>
-          Un_cv (fun n:nat => sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) l)).
+    cut { l:R | Un_cv (fun n => sum_f_R0 (fun l => fn (S N + l)%nat x) n) l }.
   intro X;
-    cut
-      (sigT
-        (fun l:R =>
-          Un_cv (fun n:nat => sum_f_R0 (fun l:nat => An (S N + l)%nat) n) l)).
+    cut { l:R | Un_cv (fun n => sum_f_R0 (fun l => An (S N + l)%nat) n) l }.
   intro X0; elim X; intros l1N H2.
   elim X0; intros l2N H3.
   cut (l1 - SP fn N x = l1N).
@@ -131,7 +125,7 @@ Proof.
   apply le_lt_n_Sm.
   apply le_plus_l.
   apply le_O_n.
-  apply existT with (l2 - sum_f_R0 An N).
+  exists (l2 - sum_f_R0 An N).
   unfold Un_cv in H0; unfold Un_cv in |- *; intros.
   elim (H0 eps H2); intros N0 H3.
   unfold R_dist in H3; exists N0; intros.
@@ -167,7 +161,7 @@ Proof.
   apply le_lt_n_Sm.
   apply le_plus_l.
   apply le_O_n.
-  apply existT with (l1 - SP fn N x).
+  exists (l1 - SP fn N x).
   unfold Un_cv in H; unfold Un_cv in |- *; intros.
   elim (H eps H2); intros N0 H3.
   unfold R_dist in H3; exists N0; intros.
@@ -216,8 +210,8 @@ Qed.
 Lemma Rseries_CV_comp :
   forall An Bn:nat -> R,
     (forall n:nat, 0 <= An n <= Bn n) ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 Bn N) l) ->
-    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
+    { l:R | Un_cv (fun N:nat => sum_f_R0 Bn N) l } ->
+    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
 Proof.
   intros An Bn H X; apply cv_cauchy_2.
   assert (H0 := cv_cauchy_1 _ X).
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index ff0a72e8..13be46da 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sqrt_reg.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Sqrt_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
-Require Import R_sqrt. Open Local Scope R_scope.
+Require Import R_sqrt. 
+Open Local Scope R_scope.
 
 (**********)
 Lemma sqrt_var_maj :
@@ -309,7 +310,7 @@ Qed.
 Lemma derivable_pt_sqrt : forall x:R, 0 < x -> derivable_pt sqrt x.
 Proof.
   unfold derivable_pt in |- *; intros.
-  apply existT with (/ (2 * sqrt x)).
+  exists (/ (2 * sqrt x)).
   apply derivable_pt_lim_sqrt; assumption.
 Qed.