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/Rtrigo_alt.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/Rtrigo_alt.v')
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index c40cc4da3..37a908037 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -55,7 +55,7 @@ Replace (sum_f_R0 [i:nat](sin_term a (S i)) (mult (S (S O)) n)) with ``-(sum_f_R Replace (sum_f_R0 [i:nat](sin_term a (S i)) (S (mult (S (S O)) n))) with ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))``. Cut ``(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))<=a-(sin a)<=(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))``->`` -(sum_f_R0 (tg_alt Un) (mult (S (S O)) n)) <= (sin a)-a <= -(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))``. Intro; Apply H2. -Apply sommes_partielles_ineq. +Apply alternated_series_ineq. Unfold Un_decreasing Un; Intro; Cut (plus (mult (S (S O)) (S (S n0))) (S O))=(S (S (plus (mult (S (S O)) (S n0)) (S O)))). Intro; Rewrite H3. Replace ``(pow a (S (S (plus (mult (S (S O)) (S n0)) (S O)))))`` with ``(pow a (plus (mult (S (S O)) (S n0)) (S O)))*(a*a)``. @@ -185,7 +185,7 @@ Replace (sum_f_R0 [i:nat](cos_term a0 (S i)) (mult (S (S O)) n0)) with ``-(sum_f Replace (sum_f_R0 [i:nat](cos_term a0 (S i)) (S (mult (S (S O)) n0))) with ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))``. Cut ``(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))<=1-(cos a0)<=(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))``->`` -(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0)) <= (cos a0)-1 <= -(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))``. Intro; Apply H3. -Apply sommes_partielles_ineq. +Apply alternated_series_ineq. Unfold Un_decreasing; Intro; Unfold Un. Cut (mult (S (S O)) (S (S n1)))=(S (S (mult (S (S O)) (S n1)))). Intro; Rewrite H4; Replace ``(pow a0 (S (S (mult (S (S O)) (S n1)))))`` with ``(pow a0 (mult (S (S O)) (S n1)))*(a0*a0)``. |