diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-22 14:23:28 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-22 14:23:28 +0000 |
| commit | 7aad4a091212f693a26539a62bf923085cedca71 (patch) | |
| tree | 1873106a034647d12a5ffb10521ccea44f4fec8a /test-suite | |
| parent | 5e73d8b29137356756e3d70fd2f009cf04141c28 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2908 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Reg.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v index 1284be48a..b088321d3 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 |