diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 16:06:20 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 16:06:20 +0000 |
| commit | 92bac4d9048a189113469516744db34af82cc421 (patch) | |
| tree | 70f19f936cc3b630a9bb6d08223347bfbe756eb5 /theories/Reals/Rpower.v | |
| parent | 785771ebd3f16778712828bee0aba79bb01e6525 (diff) | |
Renommage dans AltSeries.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3558 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 5de89f939..b280c0c0c 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -39,7 +39,7 @@ Apply Rle_monotony_contra with ``/3``. Apply Rlt_Rinv; Sup0. Rewrite Rmult_1r; Rewrite <- (Rmult_sym ``3``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. Rewrite Rmult_1l; Replace ``/(exp 1)`` with ``(exp (-1))``. -Unfold exp; Case (exist_exp ``-1``); Intros; Simpl; Unfold exp_in in e; Assert H := (sommes_partielles_ineq [i:nat]``/(INR (fact i))`` x (S O)). +Unfold exp; Case (exist_exp ``-1``); Intros; Simpl; Unfold exp_in in e; Assert H := (alternated_series_ineq [i:nat]``/(INR (fact i))`` x (S O)). Cut ``(sum_f_R0 (tg_alt [([i:nat]``/(INR (fact i))``)]) (S (mult (S (S O)) (S O)))) <= x <= (sum_f_R0 (tg_alt [([i:nat]``/(INR (fact i))``)]) (mult (S (S O)) (S O)))``. Intro; Elim H0; Clear H0; Intros H0 _; Simpl in H0; Unfold tg_alt in H0; Simpl in H0. Replace ``/3`` with ``1*/1+ -1*1*/1+ -1*( -1*1)*/2+ -1*( -1*( -1*1))*/(2+1+1+1+1)``. |