From 7aad4a091212f693a26539a62bf923085cedca71 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Mon, 22 Jul 2002 14:23:28 +0000
Subject: *** empty log message ***

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

diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v
index 1284be48ad..b088321d36 100644
--- a/test-suite/success/Reg.v
+++ b/test-suite/success/Reg.v
@@ -123,4 +123,14 @@ Lemma essai23 : (continuity_pt [x:R]``(sin (sqrt (x-1)))+(exp (Rsqr ((sqrt x)+3)
 Reg().
 Left; Apply Rlt_R0_R1.
 Right; Unfold Rminus; Rewrite Rplus_Ropp_r; Reflexivity.
+Qed.
+
+Lemma essai24 : (derivable [x:R]``(sqrt (x*x+2*x+2))+(Rabsolu (x*x+1))``).
+Reg ().
+Replace ``x*x+2*x+2`` with ``(Rsqr (x+1))+1``.
+Apply ge0_plus_gt0_is_gt0; [Apply pos_Rsqr | Apply Rlt_R0_R1].
+Unfold Rsqr; Ring.
+Red; Intro; Cut ``0<x*x+1``.
+Intro; Rewrite H in H0; Elim (Rlt_antirefl ? H0).
+Apply ge0_plus_gt0_is_gt0; [Replace ``x*x`` with (Rsqr x); [Apply pos_Rsqr | Reflexivity] | Apply Rlt_R0_R1].
 Qed.
\ No newline at end of file
-- 
cgit v1.2.3