diff options
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 |