diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 16:45:48 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 16:45:48 +0000 |
| commit | 37e7da6a31dc353db67ec18938df89b07ff9e17f (patch) | |
| tree | 22200b9f502044a044225eb31c2b2a5b6b44955d /theories/Reals/Rpower.v | |
| parent | 1a121610f8bc6761fea9dd4c41ed5255e37db657 (diff) | |
Renommage dans MVT
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3564 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 b280c0c0c..0f213e05e 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -110,7 +110,7 @@ Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H H2)). Qed. Lemma exp_ineq1 : (x:R) ``0<x`` -> ``1+x < (exp x)``. -Intros; Apply Rlt_anti_compatibility with ``-(exp 0)``; Rewrite <- (Rplus_sym (exp x)); Assert H0 := (TAF exp R0 x derivable_exp H); Elim H0; Intros; Elim H1; Intros; Unfold Rminus in H2; Rewrite H2; Rewrite Ropp_O; Rewrite Rplus_Or; Replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0). +Intros; Apply Rlt_anti_compatibility with ``-(exp 0)``; Rewrite <- (Rplus_sym (exp x)); Assert H0 := (MVT_cor1 exp R0 x derivable_exp H); Elim H0; Intros; Elim H1; Intros; Unfold Rminus in H2; Rewrite H2; Rewrite Ropp_O; Rewrite Rplus_Or; Replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0). Rewrite exp_0; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Pattern 1 x; Rewrite <- Rmult_1r; Rewrite (Rmult_sym (exp x0)); Apply Rlt_monotony. Apply H. Rewrite <- exp_0; Apply exp_increasing; Elim H3; Intros; Assumption. |