diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 14:22:44 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 14:22:44 +0000 |
| commit | a6765b2a23cbfb2c22718c1b3d7ca22e19a26c2d (patch) | |
| tree | d36cda749d530324f6b9cd6a05147a1d07d6af47 /theories/Reals/Rpower.v | |
| parent | 509442d374432f3b49e77b0f90ff80519e1e4dfd (diff) | |
Renommage f_pos -> IVT (Intermediate Value Theorem
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3583 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 5ac341355..a700d0848 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -121,7 +121,7 @@ Intros; Pose f := [x:R]``(exp x)-y``; Cut ``(f 0)<=0``. Intro; Cut (continuity f). Intro; Cut ``0<=(f y)``. Intro; Cut ``(f 0)*(f y)<=0``. -Intro; Assert X := (f_pos_cor f R0 y H2 (Rlt_le ? ? H) H4); Elim X; Intros t H5; Apply existTT with t; Elim H5; Intros; Unfold f in H7; Apply Rminus_eq_right; Exact H7. +Intro; Assert X := (IVT_cor f R0 y H2 (Rlt_le ? ? H) H4); Elim X; Intros t H5; Apply existTT with t; Elim H5; Intros; Unfold f in H7; Apply Rminus_eq_right; Exact H7. Pattern 2 R0; Rewrite <- (Rmult_Or (f y)); Rewrite (Rmult_sym (f R0)); Apply Rle_monotony; Assumption. Unfold f; Apply Rle_anti_compatibility with y; Left; Apply Rlt_trans with ``1+y``. Rewrite <- (Rplus_sym y); Apply Rlt_compatibility; Apply Rlt_R0_R1. |