From 1e558a3ce46468154c719eba3f6812be23ab49d7 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Tue, 16 Jul 2002 09:02:39 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2879 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Ranalysis1.v | 14 --------------
 theories/Reals/Ranalysis4.v | 16 ++++++++++++++++
 2 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 47397238d7..2b919ce65d 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -469,8 +469,6 @@ Elim H6; Intros; Unfold D_x in H10; Elim H10; Intros; Assumption.
 Elim H6; Intros; Assumption.
 Qed.
 
-Axiom derivable_pt_lim_sqrt : (x:R) ``0<x`` -> (derivable_pt_lim sqrt x ``/(2*(sqrt x))``).
-
 Axiom derivable_pt_lim_sin : (x:R) (derivable_pt_lim sin x (cos x)).
 
 Lemma derivable_pt_lim_cos : (x:R) (derivable_pt_lim cos x ``-(sin x)``).
@@ -555,12 +553,6 @@ Apply Specif.existT with ``x1*x0``.
 Apply derivable_pt_lim_comp; Assumption.
 Qed.
 
-Lemma derivable_pt_sqrt : (x:R) ``0<x`` -> (derivable_pt sqrt x).
-Unfold derivable_pt; Intros.
-Apply Specif.existT with ``/(2*(sqrt x))``.
-Apply derivable_pt_lim_sqrt; Assumption.
-Qed.
-
 Lemma derivable_pt_sin : (x:R) (derivable_pt sin x).
 Unfold derivable_pt; Intro.
 Apply Specif.existT with (cos x).
@@ -730,12 +722,6 @@ Unfold derive_pt in H0; Rewrite H0 in H4.
 Apply derivable_pt_lim_comp; Assumption.
 Qed.
 
-Lemma derive_pt_sqrt : (x:R;pr:``0<x``) ``(derive_pt sqrt x (derivable_pt_sqrt ? pr)) == /(2*(sqrt x))``. 
-Intros.
-Apply derive_pt_eq_0.
-Apply derivable_pt_lim_sqrt; Assumption.
-Qed.
-
 Lemma derive_pt_sin : (x:R) ``(derive_pt sin x (derivable_pt_sin ?))==(cos x)``.
 Intros; Apply derive_pt_eq_0.
 Apply derivable_pt_lim_sin.
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index a3ce1e4d1f..afd65a5000 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -16,9 +16,25 @@ Require Rderiv.
 Require DiscrR.
 Require Rtrigo.
 Require Ranalysis1.
+Require R_sqrt.
 Require Ranalysis2.
 Require Ranalysis3.
 
+(* sqrt *)
+Axiom derivable_pt_lim_sqrt : (x:R) ``0<x`` -> (derivable_pt_lim sqrt x ``/(2*(sqrt x))``).
+
+Lemma derivable_pt_sqrt : (x:R) ``0<x`` -> (derivable_pt sqrt x).
+Unfold derivable_pt; Intros.
+Apply Specif.existT with ``/(2*(sqrt x))``.
+Apply derivable_pt_lim_sqrt; Assumption.
+Qed.
+
+Lemma derive_pt_sqrt : (x:R;pr:``0<x``) ``(derive_pt sqrt x (derivable_pt_sqrt ? pr)) == /(2*(sqrt x))``. 
+Intros.
+Apply derive_pt_eq_0.
+Apply derivable_pt_lim_sqrt; Assumption.
+Qed.
+
 (**********)
 Lemma derivable_pt_inv : (f:R->R;x:R) ``(f x)<>0`` -> (derivable_pt f x) -> (derivable_pt (inv_fct f) x).
 Intros; Cut (derivable_pt (div_fct (fct_cte R1) f) x) -> (derivable_pt (inv_fct f) x).
-- 
cgit v1.2.3