sin_bound et cos_bound deplaces dans Rtrigo_alt

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2842 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 26 deletions

diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 70452fbe0..5c5c76567 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -19,10 +19,7 @@ Require Rsigma.
 Require Rlimit.
 Require Binome.
 Require Export Rtrigo_def.
-
-Lemma Ropp_mul3 : (r1,r2:R) ``r1*(-r2) == -(r1*r2)``.
-Intros; Rewrite <- Ropp_mul1; Ring.
-Qed.
+Require Export Rtrigo_alt.
 
 (* Here, we have the euclidian division *)
 (* This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI *)
@@ -288,33 +285,11 @@ Qed.
 (* Using series definitions of cos and sin                       *)
 (*****************************************************************)
 
-Definition sin_term [a:R] : nat->R := [i:nat] ``(pow (-1) i)*(pow a (plus (mult (S (S O)) i) (S O)))/(INR (fact (plus (mult (S (S O)) i) (S O))))``.
-
-Definition cos_term [a:R] : nat->R := [i:nat] ``(pow (-1) i)*(pow a (mult (S (S O)) i))/(INR (fact (mult (S (S O)) i)))``.
-
-Definition sin_approx [a:R;n:nat] : R := (sum_f_R0 (sin_term a) n).
-
-Definition cos_approx [a:R;n:nat] : R := (sum_f_R0 (cos_term a) n).
-
-Axiom 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))))``.
-
-Axiom 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))))``.
-
 Definition sin_lb [a:R] : R := (sin_approx a (3)).
 Definition sin_ub [a:R] : R := (sin_approx a (4)).
 Definition cos_lb [a:R] : R := (cos_approx a (3)).
 Definition cos_ub [a:R] : R := (cos_approx a (4)).
 
-Lemma PI_4 : ``PI<=4``.
-Assert H0 := (PI_ineq O).
-Elim H0; Clear H0; Intros _ H0.
-Unfold tg_alt PI_tg in H0; Simpl in H0.
-Rewrite Rinv_R1 in H0; Rewrite Rmult_1r in H0; Unfold Rdiv in H0.
-Apply Rle_monotony_contra with ``/4``.
-Apply Rlt_Rinv; Sup0.
-Rewrite <- Rinv_l_sym; [Rewrite Rmult_sym; Assumption | DiscrR].
-Qed.
-
 Lemma sin_lb_gt_0 : (a:R) ``0<a``->``a<=PI/2``->``0<(sin_lb a)``.
 Intros.
 Unfold sin_lb; Unfold sin_approx; Unfold sin_term.