(************************************************************************)
(*  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        *)
(************************************************************************)
 
(*i $Id: Rsqrt_def.v 8670 2006-03-28 22:16:14Z herbelin $ i*)

Require Import Sumbool.
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis1.
Open Local Scope R_scope.

Boxed 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) (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 :
 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 :
 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 :
 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 :
 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 :
 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 :
 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 :
 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 :
 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 :
 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 :
 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) := 2 ^ n.

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 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 (forall N:nat, INR N <= 2 ^ N).
intros.
unfold cv_infty in |- *.
intro.
case (total_order_T 0 M); intro.
elim s; intro.
set (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 :
 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 :=
  match Rle_dec 0 x with
  | left _ => true
  | right _ => false
  end.

(* Sequential caracterisation of continuity *)
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 :
 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 :
 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 :
 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 X X0.
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.
set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n).
set (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 :
 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 :
 forall y:R, 0 <= y -> sigT (fun z:R => 0 <= z /\ y = Rsqr z).
intros.
set (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 :=
  match Rsqrt_exists (nonneg y) (cond_nonneg y) with
  | existT a b => a
  end.

(**********)
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 : 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.