*** empty log message ***

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

1 files changed, 0 insertions, 14 deletions

diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 47397238d..2b919ce65 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.