Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 696 insertions, 622 deletions

diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index ebdece374..b123f1bb7 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -8,681 +8,755 @@
  
 (*i $Id$ i*)
 
-Require Sumbool.
-Require Rbase.
-Require Rfunctions.
-Require SeqSeries.
-Require Ranalysis1.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Sumbool.
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import SeqSeries.
+Require Import Ranalysis1.
 Open Local Scope R_scope.
 
-Fixpoint Dichotomy_lb [x,y:R;P:R->bool;N:nat] : R :=
-Cases N of 
-  O => x
-| (S n) => let down = (Dichotomy_lb x y P n) in let up = (Dichotomy_ub x y P n) in let z = ``(down+up)/2``  in if (P z) then down else z
-end
-with Dichotomy_ub [x,y:R;P:R->bool;N:nat] : R :=
-Cases N of 
-  O => y
-| (S n) => let down = (Dichotomy_lb x y P n) in let up = (Dichotomy_ub x y P n) in let z = ``(down+up)/2``  in if (P z) then z else up
-end.
+Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
+  match N with
+  | O => x
+  | S n =>
+      let down := Dichotomy_lb x y P n in
+      let up := Dichotomy_ub x y P n in
+      let z := (down + up) / 2 in if P z then down else z
+  end
+ 
+ with Dichotomy_ub (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
+  match N with
+  | O => y
+  | S n =>
+      let down := Dichotomy_lb x y P n in
+      let up := Dichotomy_ub x y P n in
+      let z := (down + up) / 2 in if P z then z else up
+  end.
 
-Definition dicho_lb [x,y:R;P:R->bool] : nat->R := [N:nat](Dichotomy_lb x y P N).
-Definition dicho_up [x,y:R;P:R->bool] : nat->R := [N:nat](Dichotomy_ub x y P N).
+Definition dicho_lb (x y:R) (P:R -> bool) (N:nat) : R := Dichotomy_lb x y P N.
+Definition dicho_up (x y:R) (P:R -> bool) (N:nat) : R := Dichotomy_ub x y P N.
 
 (**********)
-Lemma dicho_comp : (x,y:R;P:R->bool;n:nat) ``x<=y`` -> ``(dicho_lb x y P n)<=(dicho_up x y P n)``.
-Intros.
-Induction n.
-Simpl; Assumption.
-Simpl.
-Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``).
-Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
-Sup0.
-Pattern 1 ``2``; Rewrite Rmult_sym.
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1r.
-Rewrite double.
-Apply Rle_compatibility.
-Assumption.
-Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
-Sup0.
-Pattern 3 ``2``; Rewrite Rmult_sym.
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1r.
-Rewrite double.
-Rewrite <- (Rplus_sym (Dichotomy_ub x y P n)).
-Apply Rle_compatibility.
-Assumption.
+Lemma dicho_comp :
+ forall (x y:R) (P:R -> bool) (n:nat),
+   x <= y -> dicho_lb x y P n <= dicho_up x y P n.
+intros.
+induction  n as [| n Hrecn].
+simpl in |- *; assumption.
+simpl in |- *.
+case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
+unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
+prove_sup0.
+pattern 2 at 1 in |- *; rewrite Rmult_comm.
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
+rewrite Rmult_1_r.
+rewrite double.
+apply Rplus_le_compat_l.
+assumption.
+unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
+prove_sup0.
+pattern 2 at 3 in |- *; rewrite Rmult_comm.
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
+rewrite Rmult_1_r.
+rewrite double.
+rewrite <- (Rplus_comm (Dichotomy_ub x y P n)).
+apply Rplus_le_compat_l.
+assumption.
 Qed.
 
-Lemma dicho_lb_growing : (x,y:R;P:R->bool) ``x<=y`` -> (Un_growing (dicho_lb x y P)).
-Intros.
-Unfold Un_growing.
-Intro.
-Simpl.
-Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``).
-Right; Reflexivity.
-Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
-Sup0.
-Pattern 1 ``2``; Rewrite Rmult_sym.
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1r.
-Rewrite double.
-Apply Rle_compatibility.
-Replace (Dichotomy_ub x y P n) with (dicho_up x y P n); [Apply dicho_comp; Assumption | Reflexivity].
+Lemma dicho_lb_growing :
+ forall (x y:R) (P:R -> bool), x <= y -> Un_growing (dicho_lb x y P).
+intros.
+unfold Un_growing in |- *.
+intro.
+simpl in |- *.
+case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
+right; reflexivity.
+unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
+prove_sup0.
+pattern 2 at 1 in |- *; rewrite Rmult_comm.
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
+rewrite Rmult_1_r.
+rewrite double.
+apply Rplus_le_compat_l.
+replace (Dichotomy_ub x y P n) with (dicho_up x y P n);
+ [ apply dicho_comp; assumption | reflexivity ].
 Qed.
 
-Lemma dicho_up_decreasing : (x,y:R;P:R->bool) ``x<=y`` -> (Un_decreasing (dicho_up x y P)).
-Intros.
-Unfold Un_decreasing.
-Intro.
-Simpl.
-Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``).
-Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
-Sup0.
-Pattern 3 ``2``; Rewrite Rmult_sym.
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1r.
-Rewrite double.
-Replace (Dichotomy_ub x y P n) with (dicho_up x y P n); [Idtac | Reflexivity].
-Replace (Dichotomy_lb x y P n) with (dicho_lb x y P n); [Idtac | Reflexivity].
-Rewrite <- (Rplus_sym ``(dicho_up x y P n)``).
-Apply Rle_compatibility.
-Apply dicho_comp; Assumption.
-Right; Reflexivity.
+Lemma dicho_up_decreasing :
+ forall (x y:R) (P:R -> bool), x <= y -> Un_decreasing (dicho_up x y P).
+intros.
+unfold Un_decreasing in |- *.
+intro.
+simpl in |- *.
+case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
+unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
+prove_sup0.
+pattern 2 at 3 in |- *; rewrite Rmult_comm.
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
+rewrite Rmult_1_r.
+rewrite double.
+replace (Dichotomy_ub x y P n) with (dicho_up x y P n);
+ [ idtac | reflexivity ].
+replace (Dichotomy_lb x y P n) with (dicho_lb x y P n);
+ [ idtac | reflexivity ].
+rewrite <- (Rplus_comm (dicho_up x y P n)).
+apply Rplus_le_compat_l.
+apply dicho_comp; assumption.
+right; reflexivity.
 Qed.
 
-Lemma dicho_lb_maj_y : (x,y:R;P:R->bool) ``x<=y`` -> (n:nat)``(dicho_lb x y P n)<=y``.
-Intros.
-Induction n.
-Simpl; Assumption.
-Simpl.
-Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``).
-Assumption.
-Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
-Sup0.
-Pattern 3 ``2``; Rewrite Rmult_sym.
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1r | DiscrR].
-Rewrite double; Apply Rplus_le.
-Assumption.
-Pattern 2 y; Replace y with (Dichotomy_ub x y P O); [Idtac | Reflexivity].
-Apply decreasing_prop.
-Assert H0 := (dicho_up_decreasing x y P H).
-Assumption.
-Apply le_O_n.
+Lemma dicho_lb_maj_y :
+ forall (x y:R) (P:R -> bool), x <= y -> forall n:nat, dicho_lb x y P n <= y.
+intros.
+induction  n as [| n Hrecn].
+simpl in |- *; assumption.
+simpl in |- *.
+case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
+assumption.
+unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
+prove_sup0.
+pattern 2 at 3 in |- *; rewrite Rmult_comm.
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ rewrite Rmult_1_r | discrR ].
+rewrite double; apply Rplus_le_compat.
+assumption.
+pattern y at 2 in |- *; replace y with (Dichotomy_ub x y P 0);
+ [ idtac | reflexivity ].
+apply decreasing_prop.
+assert (H0 := dicho_up_decreasing x y P H).
+assumption.
+apply le_O_n.
 Qed.
 
-Lemma dicho_lb_maj : (x,y:R;P:R->bool) ``x<=y`` -> (has_ub (dicho_lb x y P)).
-Intros.
-Cut (n:nat)``(dicho_lb x y P n)<=y``.
-Intro.
-Unfold has_ub.
-Unfold bound.
-Exists y.
-Unfold is_upper_bound.
-Intros.
-Elim H1; Intros.
-Rewrite H2; Apply H0.
-Apply dicho_lb_maj_y; Assumption.
+Lemma dicho_lb_maj :
+ forall (x y:R) (P:R -> bool), x <= y -> has_ub (dicho_lb x y P).
+intros.
+cut (forall n:nat, dicho_lb x y P n <= y).
+intro.
+unfold has_ub in |- *.
+unfold bound in |- *.
+exists y.
+unfold is_upper_bound in |- *.
+intros.
+elim H1; intros.
+rewrite H2; apply H0.
+apply dicho_lb_maj_y; assumption.
 Qed.
 
-Lemma dicho_up_min_x : (x,y:R;P:R->bool) ``x<=y`` -> (n:nat)``x<=(dicho_up x y P n)``.
-Intros.
-Induction n.
-Simpl; Assumption.
-Simpl.
-Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``).
-Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
-Sup0.
-Pattern 1 ``2``; Rewrite Rmult_sym.
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1r | DiscrR].
-Rewrite double; Apply Rplus_le.
-Pattern 1 x; Replace x with (Dichotomy_lb x y P O); [Idtac | Reflexivity].
-Apply tech9.
-Assert H0 := (dicho_lb_growing x y P H).
-Assumption.
-Apply le_O_n.
-Assumption.
-Assumption.
+Lemma dicho_up_min_x :
+ forall (x y:R) (P:R -> bool), x <= y -> forall n:nat, x <= dicho_up x y P n.
+intros.
+induction  n as [| n Hrecn].
+simpl in |- *; assumption.
+simpl in |- *.
+case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
+unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
+prove_sup0.
+pattern 2 at 1 in |- *; rewrite Rmult_comm.
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ rewrite Rmult_1_r | discrR ].
+rewrite double; apply Rplus_le_compat.
+pattern x at 1 in |- *; replace x with (Dichotomy_lb x y P 0);
+ [ idtac | reflexivity ].
+apply tech9.
+assert (H0 := dicho_lb_growing x y P H).
+assumption.
+apply le_O_n.
+assumption.
+assumption.
 Qed.
 
-Lemma dicho_up_min : (x,y:R;P:R->bool) ``x<=y`` -> (has_lb (dicho_up x y P)).
-Intros.
-Cut (n:nat)``x<=(dicho_up x y P n)``.
-Intro.
-Unfold has_lb.
-Unfold bound.
-Exists ``-x``.
-Unfold is_upper_bound.
-Intros.
-Elim H1; Intros.
-Rewrite H2.
-Unfold opp_seq.
-Apply Rle_Ropp1.
-Apply H0.
-Apply dicho_up_min_x; Assumption.
+Lemma dicho_up_min :
+ forall (x y:R) (P:R -> bool), x <= y -> has_lb (dicho_up x y P).
+intros.
+cut (forall n:nat, x <= dicho_up x y P n).
+intro.
+unfold has_lb in |- *.
+unfold bound in |- *.
+exists (- x).
+unfold is_upper_bound in |- *.
+intros.
+elim H1; intros.
+rewrite H2.
+unfold opp_seq in |- *.
+apply Ropp_le_contravar.
+apply H0.
+apply dicho_up_min_x; assumption.
 Qed.
 
-Lemma dicho_lb_cv : (x,y:R;P:R->bool) ``x<=y`` -> (sigTT R [l:R](Un_cv (dicho_lb x y P) l)).
-Intros.
-Apply growing_cv.
-Apply dicho_lb_growing; Assumption.
-Apply dicho_lb_maj; Assumption.
+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).
+intros.
+apply growing_cv.
+apply dicho_lb_growing; assumption.
+apply dicho_lb_maj; assumption.
 Qed.
 
-Lemma dicho_up_cv : (x,y:R;P:R->bool) ``x<=y`` -> (sigTT R [l:R](Un_cv (dicho_up x y P) l)).
-Intros.
-Apply decreasing_cv.
-Apply dicho_up_decreasing; Assumption.
-Apply dicho_up_min; Assumption.
+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).
+intros.
+apply decreasing_cv.
+apply dicho_up_decreasing; assumption.
+apply dicho_up_min; assumption.
 Qed.
 
-Lemma dicho_lb_dicho_up : (x,y:R;P:R->bool;n:nat) ``x<=y`` -> ``(dicho_up x y P n)-(dicho_lb x y P n)==(y-x)/(pow 2 n)``.
-Intros.
-Induction n.
-Simpl.
-Unfold Rdiv; Rewrite Rinv_R1; Ring.
-Simpl.
-Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``).
-Unfold Rdiv.
-Replace ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))*/2-
-   (Dichotomy_lb x y P n)`` with ``((dicho_up x y P n)-(dicho_lb x y P n))/2``.
-Unfold Rdiv; Rewrite Hrecn.
-Unfold Rdiv.
-Rewrite Rinv_Rmult.
-Ring.
-DiscrR.
-Apply pow_nonzero; DiscrR.
-Pattern 2 (Dichotomy_lb x y P n); Rewrite (double_var (Dichotomy_lb x y P n)); Unfold dicho_up dicho_lb Rminus Rdiv; Ring.
-Replace ``(Dichotomy_ub x y P n)-((Dichotomy_lb x y P n)+
-   (Dichotomy_ub x y P n))/2`` with ``((dicho_up x y P n)-(dicho_lb x y P n))/2``.
-Unfold Rdiv; Rewrite Hrecn.
-Unfold Rdiv.
-Rewrite Rinv_Rmult.
-Ring.
-DiscrR.
-Apply pow_nonzero; DiscrR.
-Pattern 1 (Dichotomy_ub x y P n); Rewrite (double_var (Dichotomy_ub x y P n)); Unfold dicho_up dicho_lb Rminus Rdiv; Ring.
+Lemma dicho_lb_dicho_up :
+ forall (x y:R) (P:R -> bool) (n:nat),
+   x <= y -> dicho_up x y P n - dicho_lb x y P n = (y - x) / 2 ^ n.
+intros.
+induction  n as [| n Hrecn].
+simpl in |- *.
+unfold Rdiv in |- *; rewrite Rinv_1; ring.
+simpl in |- *.
+case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
+unfold Rdiv in |- *.
+replace
+ ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) * / 2 - Dichotomy_lb x y P n)
+ with ((dicho_up x y P n - dicho_lb x y P n) / 2).
+unfold Rdiv in |- *; rewrite Hrecn.
+unfold Rdiv in |- *.
+rewrite Rinv_mult_distr.
+ring.
+discrR.
+apply pow_nonzero; discrR.
+pattern (Dichotomy_lb x y P n) at 2 in |- *;
+ rewrite (double_var (Dichotomy_lb x y P n));
+ unfold dicho_up, dicho_lb, Rminus, Rdiv in |- *; ring.
+replace
+ (Dichotomy_ub x y P n - (Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)
+ with ((dicho_up x y P n - dicho_lb x y P n) / 2).
+unfold Rdiv in |- *; rewrite Hrecn.
+unfold Rdiv in |- *.
+rewrite Rinv_mult_distr.
+ring.
+discrR.
+apply pow_nonzero; discrR.
+pattern (Dichotomy_ub x y P n) at 1 in |- *;
+ rewrite (double_var (Dichotomy_ub x y P n));
+ unfold dicho_up, dicho_lb, Rminus, Rdiv in |- *; ring.
 Qed.
 
-Definition pow_2_n := [n:nat](pow ``2`` n).
+Definition pow_2_n (n:nat) := 2 ^ n.
 
-Lemma pow_2_n_neq_R0 : (n:nat) ``(pow_2_n n)<>0``.
-Intro.
-Unfold pow_2_n.
-Apply pow_nonzero.
-DiscrR.
+Lemma pow_2_n_neq_R0 : forall n:nat, pow_2_n n <> 0.
+intro.
+unfold pow_2_n in |- *.
+apply pow_nonzero.
+discrR.
 Qed.
 
-Lemma pow_2_n_growing : (Un_growing pow_2_n).
-Unfold Un_growing.
-Intro.
-Replace (S n) with (plus n (1)); [Unfold pow_2_n; Rewrite pow_add | Ring].
-Pattern 1 (pow ``2`` n); Rewrite <- Rmult_1r.
-Apply Rle_monotony.
-Left; Apply pow_lt; Sup0.
-Simpl.
-Rewrite Rmult_1r.
-Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply Rlt_R0_R1.
+Lemma pow_2_n_growing : Un_growing pow_2_n.
+unfold Un_growing in |- *.
+intro.
+replace (S n) with (n + 1)%nat;
+ [ unfold pow_2_n in |- *; rewrite pow_add | ring ].
+pattern (2 ^ n) at 1 in |- *; rewrite <- Rmult_1_r.
+apply Rmult_le_compat_l.
+left; apply pow_lt; prove_sup0.
+simpl in |- *.
+rewrite Rmult_1_r.
+pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
+ apply Rlt_0_1.
 Qed.
 
-Lemma pow_2_n_infty : (cv_infty pow_2_n).
-Cut (N:nat)``(INR N)<=(pow 2 N)``.
-Intros.
-Unfold cv_infty.
-Intro.
-Case (total_order_T R0 M); Intro.
-Elim s; Intro.
-Pose N := (up M).
-Cut `0<=N`.
-Intro.
-Elim (IZN N H0); Intros N0 H1.
-Exists N0.
-Intros.
-Apply Rlt_le_trans with (INR N0).
-Rewrite INR_IZR_INZ.
-Rewrite <- H1.
-Unfold N.
-Assert H3 := (archimed M).
-Elim H3; Intros; Assumption.
-Apply Rle_trans with (pow_2_n N0).
-Unfold pow_2_n; Apply H.
-Apply Rle_sym2.
-Apply growing_prop.
-Apply pow_2_n_growing.
-Assumption.
-Apply le_IZR.
-Unfold N.
-Simpl.
-Assert H0 := (archimed M); Elim H0; Intros.
-Left; Apply Rlt_trans with M; Assumption.
-Exists O; Intros.
-Rewrite <- b.
-Unfold pow_2_n; Apply pow_lt; Sup0.
-Exists O; Intros.
-Apply Rlt_trans with R0.
-Assumption.
-Unfold pow_2_n; Apply pow_lt; Sup0.
-Induction N.
-Simpl.
-Left; Apply Rlt_R0_R1.
-Intros.
-Pattern 2 (S n); Replace (S n) with (plus n (1)); [Idtac | Ring].
-Rewrite S_INR; Rewrite pow_add.
-Simpl.
-Rewrite Rmult_1r.
-Apply Rle_trans with ``(pow 2 n)``.
-Rewrite <- (Rplus_sym R1).
-Rewrite <- (Rmult_1r (INR n)).
-Apply (poly n R1).
-Apply Rlt_R0_R1.
-Pattern 1 (pow ``2`` n); Rewrite <- Rplus_Or.
-Rewrite <- (Rmult_sym ``2``).
-Rewrite double.
-Apply Rle_compatibility.
-Left; Apply pow_lt; Sup0.
+Lemma pow_2_n_infty : cv_infty pow_2_n.
+cut (forall N:nat, INR N <= 2 ^ N).
+intros.
+unfold cv_infty in |- *.
+intro.
+case (total_order_T 0 M); intro.
+elim s; intro.
+pose (N := up M).
+cut (0 <= N)%Z.
+intro.
+elim (IZN N H0); intros N0 H1.
+exists N0.
+intros.
+apply Rlt_le_trans with (INR N0).
+rewrite INR_IZR_INZ.
+rewrite <- H1.
+unfold N in |- *.
+assert (H3 := archimed M).
+elim H3; intros; assumption.
+apply Rle_trans with (pow_2_n N0).
+unfold pow_2_n in |- *; apply H.
+apply Rge_le.
+apply growing_prop.
+apply pow_2_n_growing.
+assumption.
+apply le_IZR.
+unfold N in |- *.
+simpl in |- *.
+assert (H0 := archimed M); elim H0; intros.
+left; apply Rlt_trans with M; assumption.
+exists 0%nat; intros.
+rewrite <- b.
+unfold pow_2_n in |- *; apply pow_lt; prove_sup0.
+exists 0%nat; intros.
+apply Rlt_trans with 0.
+assumption.
+unfold pow_2_n in |- *; apply pow_lt; prove_sup0.
+simple induction N.
+simpl in |- *.
+left; apply Rlt_0_1.
+intros.
+pattern (S n) at 2 in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ].
+rewrite S_INR; rewrite pow_add.
+simpl in |- *.
+rewrite Rmult_1_r.
+apply Rle_trans with (2 ^ n).
+rewrite <- (Rplus_comm 1).
+rewrite <- (Rmult_1_r (INR n)).
+apply (poly n 1).
+apply Rlt_0_1.
+pattern (2 ^ n) at 1 in |- *; rewrite <- Rplus_0_r.
+rewrite <- (Rmult_comm 2).
+rewrite double.
+apply Rplus_le_compat_l.
+left; apply pow_lt; prove_sup0.
 Qed.
 
-Lemma cv_dicho : (x,y,l1,l2:R;P:R->bool) ``x<=y`` -> (Un_cv (dicho_lb x y P) l1) -> (Un_cv (dicho_up x y P) l2) -> l1==l2.
-Intros.
-Assert H2 := (CV_minus ? ? ? ? H0 H1).
-Cut (Un_cv [i:nat]``(dicho_lb x y P i)-(dicho_up x y P i)`` R0).
-Intro.
-Assert H4 := (UL_sequence ? ? ? H2 H3).
-Symmetry; Apply Rminus_eq_right; Assumption.
-Unfold Un_cv; Unfold R_dist.
-Intros.
-Assert H4 := (cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty).
-Case (total_order_T x y); Intro.
-Elim s; Intro.
-Unfold Un_cv in H4; Unfold R_dist in H4.
-Cut ``0<y-x``.
-Intro Hyp.
-Cut ``0<eps/(y-x)``.
-Intro.
-Elim (H4 ``eps/(y-x)`` H5); Intros N H6.
-Exists N; Intros.
-Replace ``(dicho_lb x y P n)-(dicho_up x y P n)-0`` with ``(dicho_lb x y P n)-(dicho_up x y P n)``; [Idtac | Ring].
-Rewrite <- Rabsolu_Ropp.
-Rewrite Ropp_distr3.
-Rewrite dicho_lb_dicho_up.
-Unfold Rdiv; Rewrite Rabsolu_mult.
-Rewrite (Rabsolu_right ``y-x``).
-Apply Rlt_monotony_contra with ``/(y-x)``.
-Apply Rlt_Rinv; Assumption.
-Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1l.
-Replace ``/(pow 2 n)`` with ``/(pow 2 n)-0``; [Unfold pow_2_n Rdiv in H6; Rewrite <- (Rmult_sym eps); Apply H6; Assumption | Ring].
-Red; Intro; Rewrite H8 in Hyp; Elim (Rlt_antirefl ? Hyp).
-Apply Rle_sym1.
-Apply Rle_anti_compatibility with x; Rewrite Rplus_Or.
-Replace ``x+(y-x)`` with y; [Assumption | Ring].
-Assumption.
-Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Assumption].
-Apply Rlt_anti_compatibility with x; Rewrite Rplus_Or.
-Replace ``x+(y-x)`` with y; [Assumption | Ring].
-Exists O; Intros.
-Replace ``(dicho_lb x y P n)-(dicho_up x y P n)-0`` with ``(dicho_lb x y P n)-(dicho_up x y P n)``; [Idtac | Ring].
-Rewrite <- Rabsolu_Ropp.
-Rewrite Ropp_distr3.
-Rewrite dicho_lb_dicho_up.
-Rewrite b.
-Unfold Rminus Rdiv; Rewrite Rplus_Ropp_r; Rewrite Rmult_Ol; Rewrite Rabsolu_R0; Assumption.
-Assumption.
-Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)).
+Lemma cv_dicho :
+ forall (x y l1 l2:R) (P:R -> bool),
+   x <= y ->
+   Un_cv (dicho_lb x y P) l1 -> Un_cv (dicho_up x y P) l2 -> l1 = l2.
+intros.
+assert (H2 := CV_minus _ _ _ _ H0 H1).
+cut (Un_cv (fun i:nat => dicho_lb x y P i - dicho_up x y P i) 0).
+intro.
+assert (H4 := UL_sequence _ _ _ H2 H3).
+symmetry  in |- *; apply Rminus_diag_uniq_sym; assumption.
+unfold Un_cv in |- *; unfold R_dist in |- *.
+intros.
+assert (H4 := cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty).
+case (total_order_T x y); intro.
+elim s; intro.
+unfold Un_cv in H4; unfold R_dist in H4.
+cut (0 < y - x).
+intro Hyp.
+cut (0 < eps / (y - x)).
+intro.
+elim (H4 (eps / (y - x)) H5); intros N H6.
+exists N; intros.
+replace (dicho_lb x y P n - dicho_up x y P n - 0) with
+ (dicho_lb x y P n - dicho_up x y P n); [ idtac | ring ].
+rewrite <- Rabs_Ropp.
+rewrite Ropp_minus_distr'.
+rewrite dicho_lb_dicho_up.
+unfold Rdiv in |- *; rewrite Rabs_mult.
+rewrite (Rabs_right (y - x)).
+apply Rmult_lt_reg_l with (/ (y - x)).
+apply Rinv_0_lt_compat; assumption.
+rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_l.
+replace (/ 2 ^ n) with (/ 2 ^ n - 0);
+ [ unfold pow_2_n, Rdiv in H6; rewrite <- (Rmult_comm eps); apply H6;
+    assumption
+ | ring ].
+red in |- *; intro; rewrite H8 in Hyp; elim (Rlt_irrefl _ Hyp).
+apply Rle_ge.
+apply Rplus_le_reg_l with x; rewrite Rplus_0_r.
+replace (x + (y - x)) with y; [ assumption | ring ].
+assumption.
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ assumption | apply Rinv_0_lt_compat; assumption ].
+apply Rplus_lt_reg_r with x; rewrite Rplus_0_r.
+replace (x + (y - x)) with y; [ assumption | ring ].
+exists 0%nat; intros.
+replace (dicho_lb x y P n - dicho_up x y P n - 0) with
+ (dicho_lb x y P n - dicho_up x y P n); [ idtac | ring ].
+rewrite <- Rabs_Ropp.
+rewrite Ropp_minus_distr'.
+rewrite dicho_lb_dicho_up.
+rewrite b.
+unfold Rminus, Rdiv in |- *; rewrite Rplus_opp_r; rewrite Rmult_0_l;
+ rewrite Rabs_R0; assumption.
+assumption.
+elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)).
 Qed.
 
-Definition cond_positivity [x:R] : bool := Cases (total_order_Rle R0 x) of 
-  (leftT _) => true 
-| (rightT _) => false end.
+Definition cond_positivity (x:R) : bool :=
+  match Rle_dec 0 x with
+  | left _ => true
+  | right _ => false
+  end.
 
 (* Sequential caracterisation of continuity *)
-Lemma continuity_seq : (f:R->R;Un:nat->R;l:R) (continuity_pt f l) -> (Un_cv Un l) -> (Un_cv [i:nat](f (Un i)) (f l)).
-Unfold continuity_pt Un_cv; Unfold continue_in.
-Unfold limit1_in.
-Unfold limit_in.
-Unfold dist.
-Simpl.
-Unfold R_dist.
-Intros.
-Elim (H eps H1); Intros alp H2.
-Elim H2; Intros.
-Elim (H0 alp H3); Intros N H5.
-Exists N; Intros.
-Case (Req_EM (Un n) l); Intro.
-Rewrite H7; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
-Apply H4.
-Split.
-Unfold D_x no_cond.
-Split.
-Trivial.
-Apply not_sym; Assumption.
-Apply H5; Assumption.
+Lemma continuity_seq :
+ forall (f:R -> R) (Un:nat -> R) (l:R),
+   continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
+unfold continuity_pt, Un_cv in |- *; unfold continue_in in |- *.
+unfold limit1_in in |- *.
+unfold limit_in in |- *.
+unfold dist in |- *.
+simpl in |- *.
+unfold R_dist in |- *.
+intros.
+elim (H eps H1); intros alp H2.
+elim H2; intros.
+elim (H0 alp H3); intros N H5.
+exists N; intros.
+case (Req_dec (Un n) l); intro.
+rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
+ assumption.
+apply H4.
+split.
+unfold D_x, no_cond in |- *.
+split.
+trivial.
+apply (sym_not_eq (A:=R)); assumption.
+apply H5; assumption.
 Qed.
 
-Lemma dicho_lb_car : (x,y:R;P:R->bool;n:nat) (P x)=false -> (P (dicho_lb x y P n))=false.
-Intros.
-Induction n.
-Simpl.
-Assumption.
-Simpl.
-Assert X := (sumbool_of_bool (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``)).
-Elim X; Intro.
-Rewrite a.
-Unfold dicho_lb in Hrecn; Assumption.
-Rewrite b.
-Assumption.
+Lemma dicho_lb_car :
+ forall (x y:R) (P:R -> bool) (n:nat),
+   P x = false -> P (dicho_lb x y P n) = false.
+intros.
+induction  n as [| n Hrecn].
+simpl in |- *.
+assumption.
+simpl in |- *.
+assert
+ (X :=
+  sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))).
+elim X; intro.
+rewrite a.
+unfold dicho_lb in Hrecn; assumption.
+rewrite b.
+assumption.
 Qed.
 
-Lemma dicho_up_car : (x,y:R;P:R->bool;n:nat) (P y)=true -> (P (dicho_up x y P n))=true.
-Intros.
-Induction n.
-Simpl.
-Assumption.
-Simpl.
-Assert X := (sumbool_of_bool (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``)).
-Elim X; Intro.
-Rewrite a.
-Unfold dicho_lb in Hrecn; Assumption.
-Rewrite b.
-Assumption.
+Lemma dicho_up_car :
+ forall (x y:R) (P:R -> bool) (n:nat),
+   P y = true -> P (dicho_up x y P n) = true.
+intros.
+induction  n as [| n Hrecn].
+simpl in |- *.
+assumption.
+simpl in |- *.
+assert
+ (X :=
+  sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))).
+elim X; intro.
+rewrite a.
+unfold dicho_lb in Hrecn; assumption.
+rewrite b.
+assumption.
 Qed.
 
 (* Intermediate Value Theorem *)
-Lemma IVT : (f:R->R;x,y:R) (continuity f) -> ``x<y`` -> ``(f x)<0`` -> ``0<(f y)`` -> (sigTT R [z:R]``x<=z<=y``/\``(f z)==0``).
-Intros.
-Cut ``x<=y``.
-Intro.
-Generalize (dicho_lb_cv x y [z:R](cond_positivity (f z)) H3). 
-Generalize (dicho_up_cv x y [z:R](cond_positivity (f z)) H3). 
-Intros.
-Elim X; Intros.
-Elim X0; Intros.
-Assert H4 := (cv_dicho ? ? ? ? ? H3 p0 p).
-Rewrite H4 in p0.
-Apply existTT with x0.
-Split.
-Split.
-Apply Rle_trans with (dicho_lb x y [z:R](cond_positivity (f z)) O).
-Simpl.
-Right; Reflexivity.
-Apply growing_ineq.
-Apply dicho_lb_growing; Assumption.
-Assumption.
-Apply Rle_trans with (dicho_up x y [z:R](cond_positivity (f z)) O).
-Apply decreasing_ineq.
-Apply dicho_up_decreasing; Assumption.
-Assumption.
-Right; Reflexivity.
-2:Left; Assumption.
-Pose Vn := [n:nat](dicho_lb x y [z:R](cond_positivity (f z)) n).
-Pose Wn := [n:nat](dicho_up x y [z:R](cond_positivity (f z)) n).
-Cut ((n:nat)``(f (Vn n))<=0``)->``(f x0)<=0``.
-Cut ((n:nat)``0<=(f (Wn n))``)->``0<=(f x0)``.
-Intros.
-Cut (n:nat)``(f (Vn n))<=0``.
-Cut (n:nat)``0<=(f (Wn n))``.
-Intros.
-Assert H9 := (H6 H8).
-Assert H10 := (H5 H7).
-Apply Rle_antisym; Assumption.
-Intro.
-Unfold Wn.
-Cut (z:R) (cond_positivity z)=true <-> ``0<=z``.
-Intro.
-Assert H8 := (dicho_up_car x y [z:R](cond_positivity (f z)) n).
-Elim (H7 (f (dicho_up x y [z:R](cond_positivity (f z)) n))); Intros.
-Apply H9.
-Apply H8.
-Elim (H7 (f y)); Intros.
-Apply H12.
-Left; Assumption.
-Intro.
-Unfold cond_positivity.
-Case (total_order_Rle R0 z); Intro.
-Split.
-Intro; Assumption.
-Intro; Reflexivity.
-Split.
-Intro; Elim diff_false_true; Assumption.
-Intro.
-Elim n0; Assumption.
-Unfold Vn.
-Cut (z:R) (cond_positivity z)=false <-> ``z<0``.
-Intros.
-Assert H8 := (dicho_lb_car x y [z:R](cond_positivity (f z)) n).
-Left.
-Elim (H7 (f (dicho_lb x y [z:R](cond_positivity (f z)) n))); Intros.
-Apply H9.
-Apply H8.
-Elim (H7 (f x)); Intros.
-Apply H12.
-Assumption.
-Intro.
-Unfold cond_positivity.
-Case (total_order_Rle R0 z); Intro.
-Split.
-Intro; Elim diff_true_false; Assumption.
-Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H7)).
-Split.
-Intro; Auto with real.
-Intro; Reflexivity.
-Cut (Un_cv Wn x0).
-Intros.
-Assert H7 := (continuity_seq f Wn x0 (H x0) H5).
-Case (total_order_T R0 (f x0)); Intro.
-Elim s; Intro.
-Left; Assumption.
-Rewrite <- b; Right; Reflexivity.
-Unfold Un_cv in H7; Unfold R_dist in H7.
-Cut ``0< -(f x0)``.
-Intro.
-Elim (H7 ``-(f x0)`` H8); Intros.
-Cut (ge x2 x2); [Intro | Unfold ge; Apply le_n].
-Assert H11 := (H9 x2 H10).
-Rewrite Rabsolu_right in H11.
-Pattern 1 ``-(f x0)`` in H11; Rewrite <- Rplus_Or in H11.
-Unfold Rminus in H11; Rewrite (Rplus_sym (f (Wn x2))) in H11.
-Assert H12 := (Rlt_anti_compatibility ? ? ? H11).
-Assert H13 := (H6 x2).
-Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H13 H12)).
-Apply Rle_sym1; Left; Unfold Rminus; Apply ge0_plus_gt0_is_gt0.
-Apply H6.
-Exact H8.
-Apply Rgt_RO_Ropp; Assumption.
-Unfold Wn; Assumption.
-Cut (Un_cv Vn x0).
-Intros.
-Assert H7 := (continuity_seq f Vn x0 (H x0) H5).
-Case (total_order_T R0 (f x0)); Intro.
-Elim s; Intro.
-Unfold Un_cv in H7; Unfold R_dist in H7.
-Elim (H7 ``(f x0)`` a); Intros.
-Cut (ge x2 x2); [Intro | Unfold ge; Apply le_n].
-Assert H10 := (H8 x2 H9).
-Rewrite Rabsolu_left in H10.
-Pattern 2 ``(f x0)`` in H10; Rewrite <- Rplus_Or in H10.
-Rewrite Ropp_distr3 in H10.
-Unfold Rminus in H10.
-Assert H11 := (Rlt_anti_compatibility ? ? ? H10).
-Assert H12 := (H6 x2).
-Cut ``0<(f (Vn x2))``.
-Intro.
-Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H13 H12)).
-Rewrite <- (Ropp_Ropp (f (Vn x2))).
-Apply Rgt_RO_Ropp; Assumption.
-Apply Rlt_anti_compatibility with ``(f x0)-(f (Vn x2))``.
-Rewrite Rplus_Or; Replace ``(f x0)-(f (Vn x2))+((f (Vn x2))-(f x0))`` with R0; [Unfold Rminus; Apply gt0_plus_ge0_is_gt0 | Ring].
-Assumption.
-Apply Rge_RO_Ropp; Apply Rle_sym1; Apply H6.
-Right; Rewrite <- b; Reflexivity.
-Left; Assumption.
-Unfold Vn; Assumption.
+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).
+intros.
+cut (x <= y).
+intro.
+generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3). 
+generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3). 
+intros.
+elim X; intros.
+elim X0; intros.
+assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
+rewrite H4 in p0.
+apply existT with x0.
+split.
+split.
+apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0).
+simpl in |- *.
+right; reflexivity.
+apply growing_ineq.
+apply dicho_lb_growing; assumption.
+assumption.
+apply Rle_trans with (dicho_up x y (fun z:R => cond_positivity (f z)) 0).
+apply decreasing_ineq.
+apply dicho_up_decreasing; assumption.
+assumption.
+right; reflexivity.
+2: left; assumption.
+pose (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n).
+pose (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n).
+cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0).
+cut ((forall n:nat, 0 <= f (Wn n)) -> 0 <= f x0).
+intros.
+cut (forall n:nat, f (Vn n) <= 0).
+cut (forall n:nat, 0 <= f (Wn n)).
+intros.
+assert (H9 := H6 H8).
+assert (H10 := H5 H7).
+apply Rle_antisym; assumption.
+intro.
+unfold Wn in |- *.
+cut (forall z:R, cond_positivity z = true <-> 0 <= z).
+intro.
+assert (H8 := dicho_up_car x y (fun z:R => cond_positivity (f z)) n).
+elim (H7 (f (dicho_up x y (fun z:R => cond_positivity (f z)) n))); intros.
+apply H9.
+apply H8.
+elim (H7 (f y)); intros.
+apply H12.
+left; assumption.
+intro.
+unfold cond_positivity in |- *.
+case (Rle_dec 0 z); intro.
+split.
+intro; assumption.
+intro; reflexivity.
+split.
+intro; elim diff_false_true; assumption.
+intro.
+elim n0; assumption.
+unfold Vn in |- *.
+cut (forall z:R, cond_positivity z = false <-> z < 0).
+intros.
+assert (H8 := dicho_lb_car x y (fun z:R => cond_positivity (f z)) n).
+left.
+elim (H7 (f (dicho_lb x y (fun z:R => cond_positivity (f z)) n))); intros.
+apply H9.
+apply H8.
+elim (H7 (f x)); intros.
+apply H12.
+assumption.
+intro.
+unfold cond_positivity in |- *.
+case (Rle_dec 0 z); intro.
+split.
+intro; elim diff_true_false; assumption.
+intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
+split.
+intro; auto with real.
+intro; reflexivity.
+cut (Un_cv Wn x0).
+intros.
+assert (H7 := continuity_seq f Wn x0 (H x0) H5).
+case (total_order_T 0 (f x0)); intro.
+elim s; intro.
+left; assumption.
+rewrite <- b; right; reflexivity.
+unfold Un_cv in H7; unfold R_dist in H7.
+cut (0 < - f x0).
+intro.
+elim (H7 (- f x0) H8); intros.
+cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ].
+assert (H11 := H9 x2 H10).
+rewrite Rabs_right in H11.
+pattern (- f x0) at 1 in H11; rewrite <- Rplus_0_r in H11.
+unfold Rminus in H11; rewrite (Rplus_comm (f (Wn x2))) in H11.
+assert (H12 := Rplus_lt_reg_r _ _ _ H11).
+assert (H13 := H6 x2).
+elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H12)).
+apply Rle_ge; left; unfold Rminus in |- *; apply Rplus_le_lt_0_compat.
+apply H6.
+exact H8.
+apply Ropp_0_gt_lt_contravar; assumption.
+unfold Wn in |- *; assumption.
+cut (Un_cv Vn x0).
+intros.
+assert (H7 := continuity_seq f Vn x0 (H x0) H5).
+case (total_order_T 0 (f x0)); intro.
+elim s; intro.
+unfold Un_cv in H7; unfold R_dist in H7.
+elim (H7 (f x0) a); intros.
+cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ].
+assert (H10 := H8 x2 H9).
+rewrite Rabs_left in H10.
+pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10.
+rewrite Ropp_minus_distr' in H10.
+unfold Rminus in H10.
+assert (H11 := Rplus_lt_reg_r _ _ _ H10).
+assert (H12 := H6 x2).
+cut (0 < f (Vn x2)).
+intro.
+elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H13 H12)).
+rewrite <- (Ropp_involutive (f (Vn x2))).
+apply Ropp_0_gt_lt_contravar; assumption.
+apply Rplus_lt_reg_r with (f x0 - f (Vn x2)).
+rewrite Rplus_0_r; replace (f x0 - f (Vn x2) + (f (Vn x2) - f x0)) with 0;
+ [ unfold Rminus in |- *; apply Rplus_lt_le_0_compat | ring ].
+assumption.
+apply Ropp_0_ge_le_contravar; apply Rle_ge; apply H6.
+right; rewrite <- b; reflexivity.
+left; assumption.
+unfold Vn in |- *; assumption.
 Qed.
 
-Lemma IVT_cor : (f:R->R;x,y:R) (continuity f) -> ``x<=y`` -> ``(f x)*(f y)<=0`` -> (sigTT R [z:R]``x<=z<=y``/\``(f z)==0``).
-Intros.
-Case (total_order_T R0 (f x)); Intro.
-Case (total_order_T R0 (f y)); Intro.
-Elim s; Intro.
-Elim s0; Intro.
-Cut ``0<(f x)*(f y)``; [Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H1 H2)) | Apply Rmult_lt_pos; Assumption].
-Exists y.
-Split.
-Split; [Assumption | Right; Reflexivity].
-Symmetry; Exact b.
-Exists x.
-Split.
-Split; [Right; Reflexivity | Assumption].
-Symmetry; Exact b.
-Elim s; Intro.
-Cut ``x<y``.
-Intro.
-Assert H3 := (IVT (opp_fct f) x y (continuity_opp f H) H2).
-Cut ``(opp_fct f x)<0``.
-Cut ``0<(opp_fct f y)``.
-Intros.
-Elim (H3 H5 H4); Intros.
-Apply existTT with x0.
-Elim p; Intros.
-Split.
-Assumption.
-Unfold opp_fct in H7.
-Rewrite <- (Ropp_Ropp (f x0)).
-Apply eq_RoppO; Assumption.
-Unfold opp_fct; Apply Rgt_RO_Ropp; Assumption.
-Unfold opp_fct.
-Apply Rlt_anti_compatibility with (f x); Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Assumption.
-Inversion H0.
-Assumption.
-Rewrite H2 in a.
-Elim (Rlt_antirefl ? (Rlt_trans ? ? ? r a)).
-Apply existTT with x.
-Split.
-Split; [Right; Reflexivity | Assumption].
-Symmetry; Assumption.
-Case (total_order_T R0 (f y)); Intro.
-Elim s; Intro.
-Cut ``x<y``.
-Intro.
-Apply IVT; Assumption.
-Inversion H0.
-Assumption.
-Rewrite H2 in r.
-Elim (Rlt_antirefl ? (Rlt_trans ? ? ? r a)).
-Apply existTT with y.
-Split.
-Split; [Assumption | Right; Reflexivity].
-Symmetry; Assumption.
-Cut ``0<(f x)*(f y)``.
-Intro.
-Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H2 H1)).
-Rewrite <- Ropp_mul2; Apply Rmult_lt_pos; Apply Rgt_RO_Ropp; Assumption.
+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).
+intros.
+case (total_order_T 0 (f x)); intro.
+case (total_order_T 0 (f y)); intro.
+elim s; intro.
+elim s0; intro.
+cut (0 < f x * f y);
+ [ intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 H2))
+ | apply Rmult_lt_0_compat; assumption ].
+exists y.
+split.
+split; [ assumption | right; reflexivity ].
+symmetry  in |- *; exact b.
+exists x.
+split.
+split; [ right; reflexivity | assumption ].
+symmetry  in |- *; exact b.
+elim s; intro.
+cut (x < y).
+intro.
+assert (H3 := IVT (- f)%F x y (continuity_opp f H) H2).
+cut ((- f)%F x < 0).
+cut (0 < (- f)%F y).
+intros.
+elim (H3 H5 H4); intros.
+apply existT with x0.
+elim p; intros.
+split.
+assumption.
+unfold opp_fct in H7.
+rewrite <- (Ropp_involutive (f x0)).
+apply Ropp_eq_0_compat; assumption.
+unfold opp_fct in |- *; apply Ropp_0_gt_lt_contravar; assumption.
+unfold opp_fct in |- *.
+apply Rplus_lt_reg_r with (f x); rewrite Rplus_opp_r; rewrite Rplus_0_r;
+ assumption.
+inversion H0.
+assumption.
+rewrite H2 in a.
+elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
+apply existT with x.
+split.
+split; [ right; reflexivity | assumption ].
+symmetry  in |- *; assumption.
+case (total_order_T 0 (f y)); intro.
+elim s; intro.
+cut (x < y).
+intro.
+apply IVT; assumption.
+inversion H0.
+assumption.
+rewrite H2 in r.
+elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
+apply existT with y.
+split.
+split; [ assumption | right; reflexivity ].
+symmetry  in |- *; assumption.
+cut (0 < f x * f y).
+intro.
+elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H2 H1)).
+rewrite <- Rmult_opp_opp; apply Rmult_lt_0_compat;
+ apply Ropp_0_gt_lt_contravar; assumption.
 Qed.
 
 (* We can now define the square root function as the reciprocal transformation of the square root function *)
-Lemma Rsqrt_exists : (y:R) ``0<=y`` -> (sigTT R [z:R]``0<=z``/\``y==(Rsqr z)``).
-Intros.
-Pose f := [x:R]``(Rsqr x)-y``.
-Cut ``(f 0)<=0``.
-Intro.
-Cut (continuity f).
-Intro.
-Case (total_order_T y R1); Intro.
-Elim s; Intro.
-Cut ``0<=(f 1)``.
-Intro.
-Cut ``(f 0)*(f 1)<=0``.
-Intro.
-Assert X := (IVT_cor f R0 R1 H1 (Rlt_le ? ? Rlt_R0_R1) H3).
-Elim X; Intros t H4.
-Apply existTT with t.
-Elim H4; Intros.
-Split.
-Elim H5; Intros; Assumption.
-Unfold f in H6.
-Apply Rminus_eq_right; Exact H6.
-Rewrite Rmult_sym; Pattern 2 R0; Rewrite <- (Rmult_Or (f R1)).
-Apply Rle_monotony; Assumption.
-Unfold f.
-Rewrite Rsqr_1.
-Apply Rle_anti_compatibility with y.
-Rewrite Rplus_Or; Rewrite Rplus_sym; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Left; Assumption.
-Apply existTT with R1.
-Split.
-Left; Apply Rlt_R0_R1.
-Rewrite b; Symmetry; Apply Rsqr_1.
-Cut ``0<=(f y)``.
-Intro.
-Cut ``(f 0)*(f y)<=0``.
-Intro.
-Assert X := (IVT_cor f R0 y H1 H H3).
-Elim X; Intros t H4.
-Apply existTT with t.
-Elim H4; Intros.
-Split.
-Elim H5; Intros; Assumption.
-Unfold f in H6.
-Apply Rminus_eq_right; Exact H6.
-Rewrite Rmult_sym; Pattern 2 R0; Rewrite <- (Rmult_Or (f y)).
-Apply Rle_monotony; Assumption.
-Unfold f.
-Apply Rle_anti_compatibility with y.
-Rewrite Rplus_Or; Rewrite Rplus_sym; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or.
-Pattern 1 y; Rewrite <- Rmult_1r.
-Unfold Rsqr; Apply Rle_monotony.
-Assumption.
-Left; Exact r.
-Replace f with (minus_fct Rsqr (fct_cte y)).
-Apply continuity_minus.
-Apply derivable_continuous; Apply derivable_Rsqr.
-Apply derivable_continuous; Apply derivable_const.
-Reflexivity.
-Unfold f; Rewrite Rsqr_O.
-Unfold Rminus; Rewrite Rplus_Ol.
-Apply Rle_sym2.
-Apply Rle_RO_Ropp; Assumption.
+Lemma Rsqrt_exists :
+ forall y:R, 0 <= y -> sigT (fun z:R => 0 <= z /\ y = Rsqr z).
+intros.
+pose (f := fun x:R => Rsqr x - y).
+cut (f 0 <= 0).
+intro.
+cut (continuity f).
+intro.
+case (total_order_T y 1); intro.
+elim s; intro.
+cut (0 <= f 1).
+intro.
+cut (f 0 * f 1 <= 0).
+intro.
+assert (X := IVT_cor f 0 1 H1 (Rlt_le _ _ Rlt_0_1) H3).
+elim X; intros t H4.
+apply existT with t.
+elim H4; intros.
+split.
+elim H5; intros; assumption.
+unfold f in H6.
+apply Rminus_diag_uniq_sym; exact H6.
+rewrite Rmult_comm; pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f 1)).
+apply Rmult_le_compat_l; assumption.
+unfold f in |- *.
+rewrite Rsqr_1.
+apply Rplus_le_reg_l with y.
+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.
+split.
+left; apply Rlt_0_1.
+rewrite b; symmetry  in |- *; apply Rsqr_1.
+cut (0 <= f y).
+intro.
+cut (f 0 * f y <= 0).
+intro.
+assert (X := IVT_cor f 0 y H1 H H3).
+elim X; intros t H4.
+apply existT with t.
+elim H4; intros.
+split.
+elim H5; intros; assumption.
+unfold f in H6.
+apply Rminus_diag_uniq_sym; exact H6.
+rewrite Rmult_comm; pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y)).
+apply Rmult_le_compat_l; assumption.
+unfold f in |- *.
+apply Rplus_le_reg_l with y.
+rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *;
+ rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
+pattern y at 1 in |- *; rewrite <- Rmult_1_r.
+unfold Rsqr in |- *; apply Rmult_le_compat_l.
+assumption.
+left; exact r.
+replace f with (Rsqr - fct_cte y)%F.
+apply continuity_minus.
+apply derivable_continuous; apply derivable_Rsqr.
+apply derivable_continuous; apply derivable_const.
+reflexivity.
+unfold f in |- *; rewrite Rsqr_0.
+unfold Rminus in |- *; rewrite Rplus_0_l.
+apply Rge_le.
+apply Ropp_0_le_ge_contravar; assumption.
 Qed.
 
 (* Definition of the square root: R+->R *)
-Definition Rsqrt [y:nonnegreal] : R := Cases (Rsqrt_exists (nonneg y) (cond_nonneg y)) of (existTT a b) => a end.
+Definition Rsqrt (y:nonnegreal) : R :=
+  match Rsqrt_exists (nonneg y) (cond_nonneg y) with
+  | existT a b => a
+  end.
 
 (**********)
-Lemma Rsqrt_positivity : (x:nonnegreal) ``0<=(Rsqrt x)``.
-Intro.
-Assert X := (Rsqrt_exists (nonneg x) (cond_nonneg x)).
-Elim X; Intros.
-Cut x0==(Rsqrt x).
-Intros.
-Elim p; Intros.
-Rewrite H in H0; Assumption.
-Unfold Rsqrt.
-Case (Rsqrt_exists x (cond_nonneg x)).
-Intros.
-Elim p; Elim a; Intros.
-Apply Rsqr_inj.
-Assumption.
-Assumption.
-Rewrite <- H0; Rewrite <- H2; Reflexivity.
+Lemma Rsqrt_positivity : forall x:nonnegreal, 0 <= Rsqrt x.
+intro.
+assert (X := Rsqrt_exists (nonneg x) (cond_nonneg x)).
+elim X; intros.
+cut (x0 = Rsqrt x).
+intros.
+elim p; intros.
+rewrite H in H0; assumption.
+unfold Rsqrt in |- *.
+case (Rsqrt_exists x (cond_nonneg x)).
+intros.
+elim p; elim a; intros.
+apply Rsqr_inj.
+assumption.
+assumption.
+rewrite <- H0; rewrite <- H2; reflexivity.
 Qed.
 
 (**********)
-Lemma Rsqrt_Rsqrt : (x:nonnegreal) ``(Rsqrt x)*(Rsqrt x)==x``.
-Intros.
-Assert X := (Rsqrt_exists (nonneg x) (cond_nonneg x)).
-Elim X; Intros.
-Cut x0==(Rsqrt x).
-Intros.
-Rewrite <- H.
-Elim p; Intros.
-Rewrite H1; Reflexivity.
-Unfold Rsqrt.
-Case (Rsqrt_exists x (cond_nonneg x)).
-Intros.
-Elim p; Elim a; Intros.
-Apply Rsqr_inj.
-Assumption.
-Assumption.
-Rewrite <- H0; Rewrite <- H2; Reflexivity.
-Qed.
+Lemma Rsqrt_Rsqrt : forall x:nonnegreal, Rsqrt x * Rsqrt x = x.
+intros.
+assert (X := Rsqrt_exists (nonneg x) (cond_nonneg x)).
+elim X; intros.
+cut (x0 = Rsqrt x).
+intros.
+rewrite <- H.
+elim p; intros.
+rewrite H1; reflexivity.
+unfold Rsqrt in |- *.
+case (Rsqrt_exists x (cond_nonneg x)).
+intros.
+elim p; elim a; intros.
+apply Rsqr_inj.
+assumption.
+assumption.
+rewrite <- H0; rewrite <- H2; reflexivity.
+Qed.
\ No newline at end of file