diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 15:49:26 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 15:49:26 +0000 |
| commit | d1e24b490ff371b83c9c9a53313ebf3674f08790 (patch) | |
| tree | f62d15a9d00cc4d0e924c061de91cb8325877a7e /theories/Reals/Rlimit.v | |
| parent | 14ab34f2e46f7f4b085932347e3f42dd9f0484e4 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rlimit.v')
| -rw-r--r-- | theories/Reals/Rlimit.v | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index cf3ba98e0..0c1ad9305 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -584,7 +584,7 @@ Unfold limit1_in;Unfold limit_in;Simpl;Intros; Save. (*********) -(* + Lemma limit_inv : (f:R->R)(D:R->Prop)(l:R)(x0:R) (limit1_in f D l x0)->~(l==R0)->(limit1_in [x:R](Rinv (f x)) D (Rinv l) x0). Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H ``(Rabsolu l)/2``). Intros delta1 H2; Elim (H ``eps*((Rsqr l)/2)``). @@ -611,7 +611,10 @@ Rewrite (Rsqr_abs l); Unfold Rsqr; Unfold Rdiv; Rewrite Rinv_Rmult. Repeat Rewrite <- Rmult_assoc; Apply Rlt_monotony_r. Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption. Apply Rlt_monotony_contra with ``(Rabsolu (f x))*(Rabsolu l)*/2``. -Repeat Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. +Repeat Apply Rmult_lt_pos. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Assumption. +Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) H17)); Unfold INR; Intro H18; Assumption | Discriminate]. Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*/(Rabsolu (f x))`` with ``(Rabsolu l)/2``. Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*(2*/(Rabsolu l))`` with ``(Rabsolu (f x))``. Assumption. @@ -625,11 +628,15 @@ Apply prod_neq_R0; Assumption. Field; Repeat Apply prod_neq_R0; Assumption. Red; Intro; Rewrite H16 in H15; Rewrite Rabsolu_R0 in H15; Cut ``0<(Rabsolu l)/2``. Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rabsolu l)/2`` ``0`` H17 H15)). -Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. +Unfold Rdiv; Apply Rmult_lt_pos. +Apply Rabsolu_pos_lt; Assumption. +Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) H17)); Unfold INR; Intro; Assumption | Discriminate]. Unfold Rdiv; Field; DiscrR. Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_r]]. Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_l]]. -Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos; [Assumption | Apply Rsqr_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. -Change ``0<(Rabsolu l)/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. +Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos. +Assumption. +Apply Rsqr_pos_lt; Assumption. +Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H3; Generalize (lt_INR_0 (2) (neq_O_lt (2) H3)); Unfold INR; Intro; Assumption | Discriminate]. +Change ``0<(Rabsolu l)/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H3; Generalize (lt_INR_0 (2) (neq_O_lt (2) H3)); Unfold INR; Intro; Assumption | Discriminate]]. Save. -*)
\ No newline at end of file |