From 514842c483d25c1038021861dc35e66d465d2f23 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Thu, 18 Jul 2002 17:01:01 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2900 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Reg.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v
index 6fefad1e21..1284be48ad 100644
--- a/test-suite/success/Reg.v
+++ b/test-suite/success/Reg.v
@@ -116,4 +116,11 @@ Assert H := d_y.
 Reg().
 Apply n_y.
 Apply d_z.
+Qed.
+
+(* Pour tester la continuite de sqrt en 0 *)
+Lemma essai23 : (continuity_pt [x:R]``(sin (sqrt (x-1)))+(exp (Rsqr ((sqrt x)+3)))`` R1).
+Reg().
+Left; Apply Rlt_R0_R1.
+Right; Unfold Rminus; Rewrite Rplus_Ropp_r; Reflexivity.
 Qed.
\ No newline at end of file
-- 
cgit v1.2.3