diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:18:40 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:18:40 +0000 |
| commit | 557df731a4ad524ebabf78359f950ae063ecef51 (patch) | |
| tree | af7d4143616583a0580f1e61eefea2d5903f44e4 /theories/Reals/Rtrigo_alt.v | |
| parent | e26750987289e8143d936ba6136446190fcc560c (diff) | |
Commentaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3587 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_alt.v')
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 99d6a736b..74526c8ee 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -37,7 +37,6 @@ Rewrite <- Rinv_l_sym; [Rewrite Rmult_sym; Assumption | DiscrR]. Qed. (**********) -(* Un encadrement de sin par ses sommes partielles sur [0;PI] *) Theorem sin_bound : (a:R; n:nat) ``0 <= a``->``a <= PI``->``(sin_approx a (plus (mult (S (S O)) n) (S O))) <= (sin a)<= (sin_approx a (mult (S (S O)) (plus n (S O))))``. Intros; Case (Req_EM a R0); Intro Hyp_a. Rewrite Hyp_a; Rewrite sin_0; Split; Right; Unfold sin_approx; Apply sum_eq_R0 Orelse (Symmetry; Apply sum_eq_R0); Intros; Unfold sin_term; Rewrite pow_add; Simpl; Unfold Rdiv; Rewrite Rmult_Ol; Ring. @@ -167,8 +166,6 @@ Inversion H; [Assumption | Elim Hyp_a; Symmetry; Assumption]. Qed. (**********) -(* Un encadrement de cos par ses sommes partielles sur [-PI/2;PI/2] *) -(* La preuve utilise bien sur la parite de cos et des sommes partielles *) Lemma cos_bound : (a:R; n:nat) `` -PI/2 <= a``->``a <= PI/2``->``(cos_approx a (plus (mult (S (S O)) n) (S O))) <= (cos a) <= (cos_approx a (mult (S (S O)) (plus n (S O))))``. Cut ((a:R; n:nat) ``0 <= a``->``a <= PI/2``->``(cos_approx a (plus (mult (S (S O)) n) (S O))) <= (cos a) <= (cos_approx a (mult (S (S O)) (plus n (S O))))``) -> ((a:R; n:nat) `` -PI/2 <= a``->``a <= PI/2``->``(cos_approx a (plus (mult (S (S O)) n) (S O))) <= (cos a) <= (cos_approx a (mult (S (S O)) (plus n (S O))))``). Intros H a n; Apply H. |