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