diff options
| author | desmettr | 2002-07-18 17:01:01 +0000 |
|---|---|---|
| committer | desmettr | 2002-07-18 17:01:01 +0000 |
| commit | 514842c483d25c1038021861dc35e66d465d2f23 (patch) | |
| tree | ad48a528949c5a10d75fe0a5af33cc1cd7902deb | |
| parent | 7484a2ab839946f7cb14be190bf92ab3bc5dcafe (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2900 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/Reg.v | 7 |
1 files changed, 7 insertions, 0 deletions
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 |