sin_bound et cos_bound sont prouves (merci les series alternees...)

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

1 files changed, 518 insertions, 0 deletions

diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
new file mode 100644
index 000000000..4815028c0
--- /dev/null
+++ b/theories/Reals/Rtrigo_alt.v
@@ -0,0 +1,518 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+ 
+(*i $Id$ i*)
+
+Require DiscrR.
+Require Rbase.
+Require Rseries.
+Require Binome.
+Require Rcomplet.
+Require Rtrigo_def.
+
+(*****************************************************************)
+(* 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).
+
+(**********)
+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.
+
+(* Un -> +oo *)
+Definition cv_infty [Un:nat->R] : Prop := (M:R)(EXT N:nat | (n:nat) (le N n) -> ``M<(Un n)``).
+
+(* Un -> +oo => /Un -> O *)
+Lemma cv_infty_cv_R0 : (Un:nat->R) ((n:nat)``(Un n)<>0``) -> (cv_infty Un) -> (Un_cv [n:nat]``/(Un n)`` R0).
+Unfold cv_infty Un_cv; Unfold R_dist; Intros.
+Elim (H0 ``/eps``); Intros N0 H2.
+Exists N0; Intros.
+Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite (Rabsolu_Rinv ? (H n)).
+Apply Rlt_monotony_contra with (Rabsolu (Un n)).
+Apply Rabsolu_pos_lt; Apply H.
+Rewrite <- Rinv_r_sym.
+Apply Rlt_monotony_contra with ``/eps``.
+Apply Rlt_Rinv; Assumption.
+Rewrite Rmult_1r; Rewrite (Rmult_sym ``/eps``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Apply Rlt_le_trans with (Un n).
+Apply H2; Assumption.
+Apply Rle_Rabsolu.
+Red; Intro; Rewrite H4 in H1; Elim (Rlt_antirefl ? H1).
+Apply Rabsolu_no_R0; Apply H.
+Qed.
+
+(**********)
+Lemma sum_eq_R0 : (An:nat->R;N:nat) ((n:nat)(le n N)->``(An n)==0``) -> (sum_f_R0 An N)==R0.
+Intros; Induction N.
+Simpl; Apply H; Apply le_n.
+Rewrite tech5; Rewrite HrecN; [Rewrite Rplus_Ol; Apply H; Apply le_n | Intros; Apply H; Apply le_trans with N; [Assumption | Apply le_n_Sn]].
+Qed.
+
+(**********)
+Lemma decreasing_prop : (Un:nat->R;m,n:nat) (Un_decreasing Un) -> (le m n) -> ``(Un n)<=(Un m)``.
+Unfold Un_decreasing; Intros.
+Induction n.
+Induction m.
+Right; Reflexivity.
+Elim (le_Sn_O ? H0).
+Cut (le m n)\/m=(S n).
+Intro; Elim H1; Intro.
+Apply Rle_trans with (Un n).
+Apply H.
+Apply Hrecn; Assumption.
+Rewrite H2; Right; Reflexivity.
+Inversion H0; [Right; Reflexivity | Left; Assumption].
+Qed.
+
+(* |x|^n/n! -> 0 *)
+Lemma cv_speed_pow_fact : (x:R) (Un_cv [n:nat]``(pow x n)/(INR (fact n))`` R0).
+Intro; Cut (Un_cv [n:nat]``(pow (Rabsolu x) n)/(INR (fact n))`` R0) -> (Un_cv [n:nat]``(pow x n)/(INR (fact n))`` ``0``).
+Intro; Apply H.
+Unfold Un_cv; Unfold R_dist; Intros; Case (Req_EM x R0); Intro.
+Exists (S O); Intros.
+Rewrite H1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_R0; Rewrite pow_ne_zero; [Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rabsolu_R0; Assumption | Red; Intro; Rewrite H3 in H2; Elim (le_Sn_n ? H2)].
+Assert H2 := (Rabsolu_pos_lt x H1); Pose M := (up (Rabsolu x)); Cut `0<=M`.
+Intro; Elim (IZN M H3); Intros M_nat H4.
+Pose Un := [n:nat]``(pow (Rabsolu x) (plus M_nat n))/(INR (fact (plus M_nat n)))``.
+Cut (Un_cv Un R0); Unfold Un_cv; Unfold R_dist; Intros.
+Elim (H5 eps H0); Intros N H6.
+Exists (plus M_nat N); Intros; Cut (EX p:nat | (ge p N)/\n=(plus M_nat p)).
+Intro; Elim H8; Intros p H9.
+Elim H9; Intros; Rewrite H11; Unfold Un in H6; Apply H6; Assumption.
+Exists (minus n M_nat).
+Split.
+Unfold ge; Apply simpl_le_plus_l with M_nat; Rewrite <- le_plus_minus.
+Assumption.
+Apply le_trans with (plus M_nat N).
+Apply le_plus_l.
+Assumption.
+Apply le_plus_minus; Apply le_trans with (plus M_nat N); [Apply le_plus_l | Assumption].
+Pose Vn := [n:nat]``(Rabsolu x)*(Un O)/(INR (S n))``.
+Cut (le (1) M_nat).
+Intro; Cut (n:nat)``0<(Un n)``.
+Intro; Cut (Un_decreasing Un).
+Intro; Cut (n:nat)``(Un (S n))<=(Vn n)``.
+Intro; Cut (Un_cv Vn R0).
+Unfold Un_cv; Unfold R_dist; Intros.
+Elim (H10 eps0 H5); Intros N1 H11.
+Exists (S N1); Intros.
+Cut (n:nat)``0<(Vn n)``.
+Intro; Apply Rle_lt_trans with ``(Rabsolu ((Vn (pred n))-0))``.
+Repeat Rewrite Rabsolu_right.
+Unfold Rminus; Rewrite Ropp_O; Do 2 Rewrite Rplus_Or; Replace n with (S (pred n)).
+Apply H9.
+Inversion H12; Simpl; Reflexivity.
+Apply Rle_sym1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Left; Apply H13.
+Apply Rle_sym1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Left; Apply H7.
+Apply H11; Unfold ge; Apply le_S_n; Replace (S (pred n)) with n; [Unfold ge in H12; Exact H12 | Inversion H12; Simpl; Reflexivity].
+Intro; Apply Rlt_le_trans with (Un (S n0)); [Apply H7 | Apply H9].
+Cut (cv_infty [n:nat](INR (S n))).
+Intro; Cut (Un_cv [n:nat]``/(INR (S n))`` R0).
+Unfold Un_cv R_dist; Intros; Unfold Vn.
+Cut ``0<eps1/((Rabsolu x)*(Un O))``.
+Intro; Elim (H11 ? H13); Intros N H14.
+Exists N; Intros; Replace ``(Rabsolu x)*(Un O)/(INR (S n))-0`` with ``((Rabsolu x)*(Un O))*(/(INR (S n))-0)``; [Idtac | Unfold Rdiv; Ring].
+Rewrite Rabsolu_mult; Apply Rlt_monotony_contra with ``/(Rabsolu ((Rabsolu x)*(Un O)))``.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt.
+Apply prod_neq_R0.
+Apply Rabsolu_no_R0; Assumption.
+Assert H16 := (H7 O); Red; Intro; Rewrite H17 in H16; Elim (Rlt_antirefl ? H16).
+Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1l.
+Replace ``/(Rabsolu ((Rabsolu x)*(Un O)))*eps1`` with ``eps1/((Rabsolu x)*(Un O))``.
+Apply H14; Assumption.
+Unfold Rdiv; Rewrite (Rabsolu_right ``(Rabsolu x)*(Un O)``).
+Apply Rmult_sym.
+Apply Rle_sym1; Apply Rmult_le_pos.
+Apply Rabsolu_pos.
+Left; Apply H7.
+Apply Rabsolu_no_R0.
+Apply prod_neq_R0; [Apply Rabsolu_no_R0; Assumption | Assert H16 := (H7 O); Red; Intro; Rewrite H17 in H16; Elim (Rlt_antirefl ? H16)].
+Unfold Rdiv; Apply Rmult_lt_pos.
+Assumption.
+Apply Rlt_Rinv; Apply Rmult_lt_pos.
+Apply Rabsolu_pos_lt; Assumption.
+Apply H7.
+Apply (cv_infty_cv_R0 [n:nat]``(INR (S n))``).
+Intro; Apply not_O_INR; Discriminate.
+Assumption.
+Unfold cv_infty; Intro; Case (total_order_T M0 R0); Intro.
+Elim s; Intro.
+Exists O; Intros.
+Apply Rlt_trans with R0; [Assumption | Apply lt_INR_0; Apply lt_O_Sn].
+Exists O; Intros; Rewrite b; Apply lt_INR_0; Apply lt_O_Sn.
+Pose M0_z := (up M0).
+Assert H10 := (archimed M0).
+Cut `0<=M0_z`.
+Intro; Elim (IZN ? H11); Intros M0_nat H12.
+Exists M0_nat; Intros.
+Apply Rlt_le_trans with (IZR M0_z).
+Elim H10; Intros; Assumption.
+Rewrite H12; Rewrite <- INR_IZR_INZ; Apply le_INR.
+Apply le_trans with n; [Assumption | Apply le_n_Sn].
+Apply le_IZR; Left; Simpl; Unfold M0_z; Apply Rlt_trans with M0; [Assumption | Elim H10; Intros; Assumption].
+Intro; Apply Rle_trans with ``(Rabsolu x)*(Un n)*/(INR (S n))``.
+Unfold Un; Replace (plus M_nat (S n)) with (plus (plus M_nat n) (1)).
+Rewrite pow_add; Replace (pow (Rabsolu x) (S O)) with (Rabsolu x); [Idtac | Simpl; Ring].
+Unfold Rdiv; Rewrite <- (Rmult_sym (Rabsolu x)); Repeat Rewrite Rmult_assoc; Repeat Apply Rle_monotony.
+Apply Rabsolu_pos.
+Left; Apply pow_lt; Assumption.
+Replace (plus (plus M_nat n) (S O)) with (S (plus M_nat n)).
+Rewrite fact_simpl; Rewrite mult_sym; Rewrite mult_INR; Rewrite Rinv_Rmult.
+Apply Rle_monotony.
+Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H10 := (sym_eq ? ? ? H9); Elim (fact_neq_0 ? H10).
+Left; Apply Rinv_lt.
+Apply Rmult_lt_pos; Apply lt_INR_0; Apply lt_O_Sn.
+Apply lt_INR; Apply lt_n_S.
+Pattern 1 n; Replace n with (plus O n); [Idtac | Reflexivity].
+Apply lt_reg_r.
+Apply lt_le_trans with (S O); [Apply lt_O_Sn | Assumption].
+Apply INR_fact_neq_0.
+Apply not_O_INR; Discriminate.
+Apply INR_eq; Rewrite S_INR; Do 3 Rewrite plus_INR; Reflexivity.
+Apply INR_eq; Do 3 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
+Unfold Vn; Rewrite Rmult_assoc; Unfold Rdiv; Rewrite (Rmult_sym (Un O)); Rewrite (Rmult_sym (Un n)).
+Repeat Apply Rle_monotony.
+Apply Rabsolu_pos.
+Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply lt_O_Sn.
+Apply decreasing_prop; [Assumption | Apply le_O_n].
+Unfold Un_decreasing; Intro; Unfold Un.
+Replace (plus M_nat (S n)) with (plus (plus M_nat n) (1)).
+Rewrite pow_add; Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony.
+Left; Apply pow_lt; Assumption.
+Replace (pow (Rabsolu x) (S O)) with (Rabsolu x); [Idtac | Simpl; Ring].
+Replace (plus (plus M_nat n) (S O)) with (S (plus M_nat n)).
+Apply Rle_monotony_contra with (INR (fact (S (plus M_nat n)))).
+Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H9 := (sym_eq ? ? ? H8); Elim (fact_neq_0 ? H9).
+Rewrite (Rmult_sym (Rabsolu x)); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1l.
+Rewrite fact_simpl; Rewrite mult_INR; Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Apply Rle_trans with (INR M_nat).
+Left; Rewrite INR_IZR_INZ.
+Rewrite <- H4; Assert H8 := (archimed (Rabsolu x)); Elim H8; Intros; Assumption.
+Apply le_INR; Apply le_trans with (S M_nat); [Apply le_n_Sn | Apply le_n_S; Apply le_plus_l].
+Apply INR_fact_neq_0.
+Apply INR_fact_neq_0.
+Apply INR_eq; Rewrite S_INR; Do 3 Rewrite plus_INR; Reflexivity.
+Apply INR_eq; Do 3 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
+Intro; Unfold Un; Unfold Rdiv; Apply Rmult_lt_pos.
+Apply pow_lt; Assumption.
+Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H8 := (sym_eq ? ? ? H7); Elim (fact_neq_0 ? H8).
+Clear Un Vn; Apply INR_le; Simpl.
+Induction M_nat.
+Assert H6 := (archimed (Rabsolu x)); Elim H6; Intros; Fold M in H6.
+Rewrite H4 in H7; Rewrite <- INR_IZR_INZ in H7.
+Simpl in H7; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H2 H7)).
+Replace R1 with (INR (S O)); [Apply le_INR | Reflexivity]; Apply le_n_S; Apply le_O_n.
+Apply le_IZR; Simpl; Left; Apply Rlt_trans with (Rabsolu x).
+Assumption.
+Elim (archimed (Rabsolu x)); Intros; Assumption.
+Unfold Un_cv; Unfold R_dist; Intros; Elim (H eps H0); Intros.
+Exists x0; Intros; Apply Rle_lt_trans with ``(Rabsolu ((pow (Rabsolu x) n)/(INR (fact n))-0))``.
+Unfold Rminus; Rewrite Ropp_O; Do 2 Rewrite Rplus_Or; Rewrite (Rabsolu_right ``(pow (Rabsolu x) n)/(INR (fact n))``).
+Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite (Rabsolu_right ``/(INR (fact n))``).
+Rewrite Pow_Rabsolu; Right; Reflexivity.
+Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H4 := (sym_eq ? ? ? H3); Elim (fact_neq_0 ? H4).
+Apply Rle_sym1; Unfold Rdiv; Apply Rmult_le_pos.
+Case (Req_EM x R0); Intro.
+Rewrite H3; Rewrite Rabsolu_R0.
+Induction n; [Simpl; Left; Apply Rlt_R0_R1 | Simpl; Rewrite Rmult_Ol; Right; Reflexivity].
+Left; Apply pow_lt; Apply Rabsolu_pos_lt; Assumption.
+Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H4 := (sym_eq ? ? ? H3); Elim (fact_neq_0 ? H4).
+Apply H1; Assumption.
+Qed.
+
+Lemma pow_Rsqr : (x:R;n:nat) (pow x (mult (2) n))==(pow (Rsqr x) n).
+Intros; Induction n.
+Reflexivity.
+Replace (mult (2) (S n)) with (S (S (mult (2) n))).
+Replace (pow x (S (S (mult (2) n)))) with ``x*x*(pow x (mult (S (S O)) n))``.
+Rewrite Hrecn; Reflexivity.
+Simpl; Ring.
+Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
+Qed.
+
+Lemma Ropp_mul3 : (r1,r2:R) ``r1*(-r2) == -(r1*r2)``.
+Intros; Rewrite <- Ropp_mul1; Ring.
+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.
+Unfold sin_approx; Cut ``0<a``.
+Intro Hyp_a_pos.
+Rewrite (decomp_sum (sin_term a) (plus (mult (S (S O)) n) (S O))).
+Rewrite (decomp_sum (sin_term a) (mult (S (S O)) (plus n (S O)))).
+Replace (sin_term a O) with a.
+Cut (Rle (sum_f_R0 [i:nat](sin_term a (S i)) (pred (plus (mult (S (S O)) n) (S O)))) ``(sin a)-a``)/\(Rle ``(sin a)-a`` (sum_f_R0 [i:nat](sin_term a (S i)) (pred (mult (S (S O)) (plus n (S O)))))) -> (Rle (Rplus a (sum_f_R0 [i:nat](sin_term a (S i)) (pred (plus (mult (S (S O)) n) (S O))))) (sin a))/\(Rle (sin a) (Rplus a (sum_f_R0 [i:nat](sin_term a (S i)) (pred (mult (S (S O)) (plus n (S O))))))).
+Intro; Apply H1.
+Pose Un := [n:nat]``(pow a (plus (mult (S (S O)) (S n)) (S O)))/(INR (fact (plus (mult (S (S O)) (S n)) (S O))))``.
+Replace (pred (plus (mult (S (S O)) n) (S O))) with (mult (S (S O)) n).
+Replace (pred (mult (S (S O)) (plus n (S O)))) with (S (mult (S (S O)) n)).
+Replace (sum_f_R0 [i:nat](sin_term a (S i)) (mult (S (S O)) n)) with ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))``.
+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.
+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)``.
+Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony.
+Left; Apply pow_lt; Assumption.
+Apply Rle_monotony_contra with ``(INR (fact (S (S (plus (mult (S (S O)) (S n0)) (S O))))))``.
+Rewrite <- H3; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H5 := (sym_eq ? ? ? H4); Elim (fact_neq_0 ? H5).
+Rewrite <- H3; Rewrite (Rmult_sym ``(INR (fact (plus (mult (S (S O)) (S (S n0))) (S O))))``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite H3; Do 2 Rewrite fact_simpl; Do 2 Rewrite mult_INR; Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r.
+Do 2 Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Simpl; Replace ``((0+1+1)*((INR n0)+1)+(0+1)+1+1)*((0+1+1)*((INR n0)+1)+(0+1)+1)`` with ``4*(INR n0)*(INR n0)+18*(INR n0)+20``; [Idtac | Ring].
+Apply Rle_trans with ``20``.
+Apply Rle_trans with ``16``.
+Replace ``16`` with ``(Rsqr 4)``; [Idtac | SqRing].
+Replace ``a*a`` with (Rsqr a); [Idtac | Reflexivity].
+Apply Rsqr_incr_1.
+Apply Rle_trans with PI; [Assumption | Apply PI_4].
+Assumption.
+Left; Sup0.
+Pattern 1 ``16``; Rewrite <- Rplus_Or; Replace ``20`` with ``16+4``; [Apply Rle_compatibility; Left; Sup0 | Ring].
+Rewrite <- (Rplus_sym ``20``); Pattern 1 ``20``; Rewrite <- Rplus_Or; Apply Rle_compatibility.
+Apply ge0_plus_ge0_is_ge0.
+Repeat Apply Rmult_le_pos.
+Left; Sup0.
+Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity].
+Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity].
+Apply Rmult_le_pos.
+Left; Sup0.
+Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity].
+Apply INR_fact_neq_0.
+Apply INR_fact_neq_0.
+Simpl; Ring.
+Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
+Assert H3 := (cv_speed_pow_fact a); Unfold Un; Unfold Un_cv in H3; Unfold R_dist in H3; Unfold Un_cv; Unfold R_dist; Intros; Elim (H3 eps H4); Intros N H5.
+Exists N; Intros; Apply H5.
+Replace (plus (mult (2) (S n0)) (1)) with (S (mult (2) (S n0))).
+Unfold ge; Apply le_trans with (mult (2) (S n0)).
+Apply le_trans with (mult (2) (S N)).
+Apply le_trans with (mult (2) N).
+Apply le_n_2n.
+Apply mult_le; Apply le_n_Sn.
+Apply mult_le; Apply le_n_S; Assumption.
+Apply le_n_Sn.
+Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Reflexivity.
+Assert X := (exist_sin (Rsqr a)); Elim X; Intros.
+Cut ``x==(sin a)/a``.
+Intro; Rewrite H3 in p; Unfold sin_in in p; Unfold infinit_sum in p; Unfold R_dist in p; Unfold Un_cv; Unfold R_dist; Intros.
+Cut ``0<eps/(Rabsolu a)``.
+Intro; Elim (p ? H5); Intros N H6.
+Exists N; Intros.
+Replace (sum_f_R0 (tg_alt Un) n0) with (Rmult a (Rminus R1 (sum_f_R0 [i:nat]``(sin_n i)*(pow (Rsqr a) i)`` (S n0)))).
+Unfold Rminus; Rewrite Rmult_Rplus_distr; Rewrite Rmult_1r; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym a); Rewrite (Rplus_sym ``-a``); Repeat Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply Rlt_monotony_contra with ``/(Rabsolu a)``.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption.
+Pattern 1 ``/(Rabsolu a)``; Rewrite <- (Rabsolu_Rinv a  Hyp_a).
+Rewrite <- Rabsolu_mult; Rewrite Rmult_Rplus_distr; Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1l | Assumption]; Rewrite (Rmult_sym ``/a``); Rewrite (Rmult_sym ``/(Rabsolu a)``); Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Unfold Rminus Rdiv in H6; Apply H6; Unfold ge; Apply le_trans with n0; [Exact H7 | Apply le_n_Sn].
+Rewrite (decomp_sum [i:nat]``(sin_n i)*(pow (Rsqr a) i)`` (S n0)).
+Replace (sin_n O) with R1.
+Simpl; Rewrite Rmult_1r; Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Rewrite Ropp_mul3; Rewrite <- Ropp_mul1; Rewrite scal_sum; Apply sum_eq.
+Intros; Unfold sin_n Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-(pow (-1) i)``.
+Replace ``(pow a (plus (mult (S (S O)) (S i)) (S O)))`` with ``(Rsqr a)*(pow (Rsqr a) i)*a``.
+Unfold Rdiv; Ring.
+Rewrite pow_add; Rewrite pow_Rsqr; Simpl; Ring.
+Simpl; Ring.
+Unfold sin_n; Unfold Rdiv; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity.
+Apply lt_O_Sn.
+Unfold Rdiv; Apply Rmult_lt_pos.
+Assumption.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption.
+Unfold sin; Case (exist_sin (Rsqr a)).
+Intros; Cut x==x0.
+Intro; Rewrite H3; Unfold Rdiv.
+Symmetry; Apply Rinv_r_simpl_m; Assumption.
+Unfold sin_in in p; Unfold sin_in in s; EApply unicite_sum.
+Apply p.
+Apply s.
+Intros; Elim H2; Intros.
+Replace ``(sin a)-a`` with ``-(a-(sin a))``; [Idtac | Ring].
+Split; Apply Rle_Ropp1; Assumption.
+Replace ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))`` with ``-1*(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))``; [Rewrite scal_sum | Ring].
+Apply sum_eq; Intros; Unfold sin_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``.
+Unfold Rdiv; Ring.
+Reflexivity.
+Replace ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))`` with ``-1*(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))``; [Rewrite scal_sum | Ring].
+Apply sum_eq; Intros.
+Unfold sin_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``.
+Unfold Rdiv; Ring.
+Reflexivity.
+Replace (mult (2) (plus n (1))) with (S (S (mult (2) n))).
+Reflexivity.
+Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring.
+Replace (plus (mult (2) n) (1)) with (S (mult (2) n)).
+Reflexivity.
+Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
+Intro; Elim H1; Intros.
+Split.
+Apply Rle_anti_compatibility with ``-a``.
+Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-a``); Apply H2.
+Apply Rle_anti_compatibility with ``-a``.
+Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-a``); Apply H3.
+Unfold sin_term; Simpl; Unfold Rdiv; Rewrite Rinv_R1; Ring.
+Replace (mult (2) (plus n (1))) with (S (S (mult (2) n))).
+Apply lt_O_Sn.
+Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring.
+Replace (plus (mult (2) n) (1)) with (S (mult (2) n)).
+Apply lt_O_Sn.
+Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
+Inversion H; [Assumption | Elim Hyp_a; Symmetry; Assumption].
+Qed.
+
+Lemma pow_le : (a:R;n:nat) ``0<=a`` -> ``0<=(pow a n)``.
+Intros; Induction n.
+Simpl; Left; Apply Rlt_R0_R1.
+Simpl; Apply Rmult_le_pos; 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.
+Intros; Unfold cos_approx.
+Rewrite (decomp_sum (cos_term a0) (plus (mult (S (S O)) n0) (S O))).
+Rewrite (decomp_sum (cos_term a0) (mult (S (S O)) (plus n0 (S O)))).
+Replace (cos_term a0 O) with R1.
+Cut (Rle (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (plus (mult (S (S O)) n0) (S O)))) ``(cos a0)-1``)/\(Rle ``(cos a0)-1`` (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (mult (S (S O)) (plus n0 (S O)))))) -> (Rle (Rplus R1 (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (plus (mult (S (S O)) n0) (S O))))) (cos a0))/\(Rle (cos a0) (Rplus R1 (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (mult (S (S O)) (plus n0 (S O))))))).
+Intro; Apply H2.
+Pose Un := [n:nat]``(pow a0 (mult (S (S O)) (S n)))/(INR (fact (mult (S (S O)) (S n))))``.
+Replace (pred (plus (mult (S (S O)) n0) (S O))) with (mult (S (S O)) n0).
+Replace (pred (mult (S (S O)) (plus n0 (S O)))) with (S (mult (S (S O)) n0)).
+Replace (sum_f_R0 [i:nat](cos_term a0 (S i)) (mult (S (S O)) n0)) with ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))``.
+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.
+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)``.
+Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony.
+Apply pow_le; Assumption.
+Apply Rle_monotony_contra with ``(INR (fact (S (S (mult (S (S O)) (S n1))))))``.
+Rewrite <- H4; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H6 := (sym_eq ? ? ? H5); Elim (fact_neq_0 ? H6).
+Rewrite <- H4; Rewrite (Rmult_sym ``(INR (fact (mult (S (S O)) (S (S n1)))))``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite H4; Do 2 Rewrite fact_simpl; Do 2 Rewrite mult_INR; Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Do 2 Rewrite S_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Simpl; Replace ``((0+1+1)*((INR n1)+1)+1+1)*((0+1+1)*((INR n1)+1)+1)`` with ``4*(INR n1)*(INR n1)+14*(INR n1)+12``; [Idtac | Ring].
+Apply Rle_trans with ``12``.
+Apply Rle_trans with ``4``.
+Replace ``4`` with ``(Rsqr 2)``; [Idtac | SqRing].
+Replace ``a0*a0`` with (Rsqr a0); [Idtac | Reflexivity].
+Apply Rsqr_incr_1.
+Apply Rle_trans with ``PI/2``.
+Assumption.
+Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
+Apply Rgt_2_0.
+Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m.
+Replace ``2*2`` with ``4``; [Apply PI_4 | Ring].
+DiscrR.
+Assumption.
+Left; Apply Rgt_2_0.
+Pattern 1 ``4``; Rewrite <- Rplus_Or; Replace ``12`` with ``4+8``; [Apply Rle_compatibility; Left; Sup0 | Ring].
+Rewrite <- (Rplus_sym ``12``); Pattern 1 ``12``; Rewrite <- Rplus_Or; Apply Rle_compatibility.
+Apply ge0_plus_ge0_is_ge0.
+Repeat Apply Rmult_le_pos.
+Left; Sup0.
+Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity].
+Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity].
+Apply Rmult_le_pos.
+Left; Sup0.
+Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity].
+Apply INR_fact_neq_0.
+Apply INR_fact_neq_0.
+Simpl; Ring.
+Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
+Assert H4 := (cv_speed_pow_fact a0); Unfold Un; Unfold Un_cv in H4; Unfold R_dist in H4; Unfold Un_cv; Unfold R_dist; Intros; Elim (H4 eps H5); Intros N H6; Exists N; Intros.
+Apply H6; Unfold ge; Apply le_trans with (mult (2) (S N)).
+Apply le_trans with (mult (2) N).
+Apply le_n_2n.
+Apply mult_le; Apply le_n_Sn.
+Apply mult_le; Apply le_n_S; Assumption.
+Assert X := (exist_cos (Rsqr a0)); Elim X; Intros.
+Cut ``x==(cos a0)``.
+Intro; Rewrite H4 in p; Unfold cos_in in p; Unfold infinit_sum in p; Unfold R_dist in p; Unfold Un_cv; Unfold R_dist; Intros.
+Elim (p ? H5); Intros N H6.
+Exists N; Intros.
+Replace (sum_f_R0 (tg_alt Un) n1) with (Rminus R1 (sum_f_R0 [i:nat]``(cos_n i)*(pow (Rsqr a0) i)`` (S n1))).
+Unfold Rminus; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym R1); Rewrite (Rplus_sym ``-1``); Repeat Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Unfold Rminus in H6; Apply H6.
+Unfold ge; Apply le_trans with n1.
+Exact H7.
+Apply le_n_Sn.
+Rewrite (decomp_sum [i:nat]``(cos_n i)*(pow (Rsqr a0) i)`` (S n1)).
+Replace (cos_n O) with R1.
+Simpl; Rewrite Rmult_1r; Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Replace (Ropp (sum_f_R0 [i:nat]``(cos_n (S i))*((Rsqr a0)*(pow (Rsqr a0) i))`` n1)) with (Rmult ``-1`` (sum_f_R0 [i:nat]``(cos_n (S i))*((Rsqr a0)*(pow (Rsqr a0) i))`` n1)); [Idtac | Ring]; Rewrite scal_sum; Apply sum_eq; Intros; Unfold cos_n Un tg_alt.
+Replace ``(pow (-1) (S i))`` with ``-(pow (-1) i)``.
+Replace ``(pow a0 (mult (S (S O)) (S i)))`` with ``(Rsqr a0)*(pow (Rsqr a0) i)``.
+Unfold Rdiv; Ring.
+Rewrite pow_Rsqr; Reflexivity.
+Simpl; Ring.
+Unfold cos_n; Unfold Rdiv; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity.
+Apply lt_O_Sn.
+Unfold cos; Case (exist_cos (Rsqr a0)); Intros; Unfold cos_in in p; Unfold cos_in in c; EApply unicite_sum.
+Apply p.
+Apply c.
+Intros; Elim H3; Intros; Replace ``(cos a0)-1`` with ``-(1-(cos a0))``; [Idtac | Ring].
+Split; Apply Rle_Ropp1; Assumption.
+Replace ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))`` with ``-1*(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))``; [Rewrite scal_sum | Ring].
+Apply sum_eq; Intros; Unfold cos_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``.
+Unfold Rdiv; Ring.
+Reflexivity.
+Replace ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))`` with ``-1*(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))``; [Rewrite scal_sum | Ring]; Apply sum_eq; Intros; Unfold cos_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``.
+Unfold Rdiv; Ring.
+Reflexivity.
+Replace (mult (2) (plus n0 (1))) with (S (S (mult (2) n0))).
+Reflexivity.
+Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring.
+Replace (plus (mult (2) n0) (1)) with (S (mult (2) n0)).
+Reflexivity.
+Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
+Intro; Elim H2; Intros; Split.
+Apply Rle_anti_compatibility with ``-1``.
+Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-1``); Apply H3.
+Apply Rle_anti_compatibility with ``-1``.
+Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-1``); Apply H4.
+Unfold cos_term; Simpl; Unfold Rdiv; Rewrite Rinv_R1; Ring.
+Replace (mult (2) (plus n0 (1))) with (S (S (mult (2) n0))).
+Apply lt_O_Sn.
+Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring.
+Replace (plus (mult (2) n0) (1)) with (S (mult (2) n0)).
+Apply lt_O_Sn.
+Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
+Intros; Case (total_order_T R0 a); Intro.
+Elim s; Intro.
+Apply H; [Left; Assumption | Assumption].
+Apply H; [Right; Assumption | Assumption].
+Cut ``0< -a``.
+Intro; Cut (x:R;n:nat) (cos_approx x n)==(cos_approx ``-x`` n).
+Intro; Rewrite H3; Rewrite (H3 a (mult (S (S O)) (plus n (S O)))); Rewrite cos_paire; Apply H.
+Left; Assumption.
+Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rle_Ropp1; Unfold Rdiv; Unfold Rdiv in H0; Rewrite <- Ropp_mul1; Exact H0.
+Intros; Unfold cos_approx; Apply sum_eq; Intros; Unfold cos_term; Do 2 Rewrite pow_Rsqr; Rewrite Rsqr_neg; Unfold Rdiv; Reflexivity.
+Apply Rgt_RO_Ropp; Assumption.
+Qed.
\ No newline at end of file