diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
| commit | bcc5b59c086d1c06a1ec03ee0bff7647338bb258 (patch) | |
| tree | 4f332b460941cdbb211806659b1fe76253f2fc67 /theories/Reals/Ranalysis3.v | |
| parent | 35cd1baf98895aa07d300d22c9e8148c91b43dac (diff) | |
Réorganisation de la librairie des réels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Ranalysis3.v')
| -rw-r--r-- | theories/Reals/Ranalysis3.v | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 2a12b2f45..5ffa915dc 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -8,13 +8,8 @@ (*i $Id$ i*) -Require Rbase. -Require Rbasic_fun. -Require R_sqr. -Require Rlimit. -Require Rderiv. -Require DiscrR. -Require Rtrigo. +Require RealsB. +Require Rfunctions. Require Ranalysis1. Require Ranalysis2. @@ -29,7 +24,7 @@ Unfold div_fct. Assert H3 := (derivable_continuous_pt ? ? X). Unfold continuity_pt in H3; Unfold continue_in in H3; Unfold limit1_in in H3; Unfold limit_in in H3; Unfold dist in H3. Simpl in H3; Unfold R_dist in H3. -Elim (H3 ``(Rabsolu (f2 x))/2``); [Idtac | Unfold Rdiv; Change ``0 < (Rabsolu (f2 x))*/2``; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]]. +Elim (H3 ``(Rabsolu (f2 x))/2``); [Idtac | Unfold Rdiv; Change ``0 < (Rabsolu (f2 x))*/2``; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Sup0]]. Clear H3; Intros alp_f2 H3. Cut (x0:R) ``(Rabsolu (x0-x)) < alp_f2`` ->``(Rabsolu ((f2 x0)-(f2 x))) < (Rabsolu (f2 x))/2``. Intro H4. @@ -539,7 +534,7 @@ Repeat Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r. Apply Rlt_monotony_contra with ``/2``. -Apply Rlt_Rinv; Apply Rgt_2_0. +Apply Rlt_Rinv; Sup0. Repeat Rewrite (Rmult_sym ``/2``). Repeat Rewrite Rmult_assoc. Rewrite <- Rinv_r_sym. @@ -565,7 +560,7 @@ Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or. Unfold Rminus in H7; Assumption. Intros. Case (Req_EM x x0); Intro. -Rewrite <- H5; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. +Rewrite <- H5; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Sup0]. Elim H3; Intros. Apply H7. Split. |