Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 399 insertions, 267 deletions

diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 4fdc39106..c1ffc68ea 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -8,287 +8,419 @@
  
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require SeqSeries.
-Require Rtrigo_def.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import SeqSeries.
+Require Import Rtrigo_def.
 Open Local Scope R_scope.
 
 (*****************************************************************)
 (* 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 sin_term (a:R) (i:nat) : R :=
+  (-1) ^ i * (a ^ (2 * i + 1) / INR (fact (2 * i + 1))).
 
-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 cos_term (a:R) (i:nat) : R :=
+  (-1) ^ i * (a ^ (2 * i) / INR (fact (2 * i))).
 
-Definition sin_approx [a:R;n:nat] : R := (sum_f_R0 (sin_term a) n).
+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).
+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].
+Lemma PI_4 : PI <= 4.
+assert (H0 := PI_ineq 0).
+elim H0; clear H0; intros _ H0.
+unfold tg_alt, PI_tg in H0; simpl in H0.
+rewrite Rinv_1 in H0; rewrite Rmult_1_r in H0; unfold Rdiv in H0.
+apply Rmult_le_reg_l with (/ 4).
+apply Rinv_0_lt_compat; prove_sup0.
+rewrite <- Rinv_l_sym; [ rewrite Rmult_comm; assumption | discrR ].
 Qed.
 
 (**********)
-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 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)``.
-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.
-Rewrite <- (Rplus_Or ``16``); 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.
-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 unicity_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].
+Theorem sin_bound :
+ forall (a:R) (n:nat),
+   0 <= a ->
+   a <= PI -> sin_approx a (2 * n + 1) <= sin a <= sin_approx a (2 * (n + 1)).
+intros; case (Req_dec a 0); intro Hyp_a.
+rewrite Hyp_a; rewrite sin_0; split; right; unfold sin_approx in |- *;
+ apply sum_eq_R0 || (symmetry  in |- *; apply sum_eq_R0); 
+ intros; unfold sin_term in |- *; rewrite pow_add; 
+ simpl in |- *; unfold Rdiv in |- *; rewrite Rmult_0_l; 
+ ring.
+unfold sin_approx in |- *; cut (0 < a).
+intro Hyp_a_pos.
+rewrite (decomp_sum (sin_term a) (2 * n + 1)).
+rewrite (decomp_sum (sin_term a) (2 * (n + 1))).
+replace (sin_term a 0) with a.
+cut
+ (sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * n + 1)) <= sin a - a /\
+  sin a - a <= sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * (n + 1))) ->
+  a + sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * n + 1)) <= sin a /\
+  sin a <= a + sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * (n + 1)))).
+intro; apply H1.
+pose (Un := fun n:nat => a ^ (2 * S n + 1) / INR (fact (2 * S n + 1))).
+replace (pred (2 * n + 1)) with (2 * n)%nat.
+replace (pred (2 * (n + 1))) with (S (2 * n)).
+replace (sum_f_R0 (fun i:nat => sin_term a (S i)) (2 * n)) with
+ (- sum_f_R0 (tg_alt Un) (2 * n)).
+replace (sum_f_R0 (fun i:nat => sin_term a (S i)) (S (2 * n))) with
+ (- sum_f_R0 (tg_alt Un) (S (2 * n))).
+cut
+ (sum_f_R0 (tg_alt Un) (S (2 * n)) <= a - sin a <=
+  sum_f_R0 (tg_alt Un) (2 * n) ->
+  - sum_f_R0 (tg_alt Un) (2 * n) <= sin a - a <=
+  - sum_f_R0 (tg_alt Un) (S (2 * n))).
+intro; apply H2.
+apply alternated_series_ineq.
+unfold Un_decreasing, Un in |- *; intro;
+ cut ((2 * S (S n0) + 1)%nat = S (S (2 * S n0 + 1))).
+intro; rewrite H3.
+replace (a ^ S (S (2 * S n0 + 1))) with (a ^ (2 * S n0 + 1) * (a * a)).
+unfold Rdiv in |- *; rewrite Rmult_assoc; apply Rmult_le_compat_l.
+left; apply pow_lt; assumption.
+apply Rmult_le_reg_l with (INR (fact (S (S (2 * S n0 + 1))))).
+rewrite <- H3; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
+ assert (H5 := sym_eq H4); elim (fact_neq_0 _ H5).
+rewrite <- H3; rewrite (Rmult_comm (INR (fact (2 * S (S n0) + 1))));
+ rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_r; rewrite H3; do 2 rewrite fact_simpl; do 2 rewrite mult_INR;
+ repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
+rewrite Rmult_1_r.
+do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR;
+ simpl in |- *;
+ 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 | ring_Rsqr ].
+replace (a * a) with (Rsqr a); [ idtac | reflexivity ].
+apply Rsqr_incr_1.
+apply Rle_trans with PI; [ assumption | apply PI_4 ].
+assumption.
+left; prove_sup0.
+rewrite <- (Rplus_0_r 16); replace 20 with (16 + 4);
+ [ apply Rplus_le_compat_l; left; prove_sup0 | ring ].
+rewrite <- (Rplus_comm 20); pattern 20 at 1 in |- *; rewrite <- Rplus_0_r;
+ apply Rplus_le_compat_l.
+apply Rplus_le_le_0_compat.
+repeat apply Rmult_le_pos.
+left; prove_sup0.
+left; prove_sup0.
+replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+apply Rmult_le_pos.
+left; prove_sup0.
+replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+apply INR_fact_neq_0.
+apply INR_fact_neq_0.
+simpl in |- *; 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 in |- *; unfold Un_cv in H3;
+ unfold R_dist in H3; unfold Un_cv in |- *; unfold R_dist in |- *; 
+ intros; elim (H3 eps H4); intros N H5.
+exists N; intros; apply H5.
+replace (2 * S n0 + 1)%nat with (S (2 * S n0)).
+unfold ge in |- *; apply le_trans with (2 * S n0)%nat.
+apply le_trans with (2 * S N)%nat.
+apply le_trans with (2 * N)%nat.
+apply le_n_2n.
+apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_Sn.
+apply (fun m n p:nat => mult_le_compat_l p n m); 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 in |- *; unfold R_dist in |- *; 
+ intros.
+cut (0 < eps / Rabs a).
+intro; elim (p _ H5); intros N H6.
+exists N; intros.
+replace (sum_f_R0 (tg_alt Un) n0) with
+ (a * (1 - sum_f_R0 (fun i:nat => sin_n i * Rsqr a ^ i) (S n0))).
+unfold Rminus in |- *; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r;
+ rewrite Ropp_plus_distr; rewrite Ropp_involutive; 
+ repeat rewrite Rplus_assoc; rewrite (Rplus_comm a);
+ rewrite (Rplus_comm (- a)); repeat rewrite Rplus_assoc; 
+ rewrite Rplus_opp_l; rewrite Rplus_0_r; apply Rmult_lt_reg_l with (/ Rabs a).
+apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption.
+pattern (/ Rabs a) at 1 in |- *; rewrite <- (Rabs_Rinv a Hyp_a).
+rewrite <- Rabs_mult; rewrite Rmult_plus_distr_l; rewrite <- Rmult_assoc;
+ rewrite <- Rinv_l_sym; [ rewrite Rmult_1_l | assumption ];
+ rewrite (Rmult_comm (/ a)); rewrite (Rmult_comm (/ Rabs a));
+ rewrite <- Rabs_Ropp; rewrite Ropp_plus_distr; rewrite Ropp_involutive;
+ unfold Rminus, Rdiv in H6; apply H6; unfold ge in |- *;
+ apply le_trans with n0; [ exact H7 | apply le_n_Sn ].
+rewrite (decomp_sum (fun i:nat => sin_n i * Rsqr a ^ i) (S n0)).
+replace (sin_n 0) with 1.
+simpl in |- *; rewrite Rmult_1_r; unfold Rminus in |- *;
+ rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; rewrite Rplus_opp_r;
+ rewrite Rplus_0_l; rewrite Ropp_mult_distr_r_reverse;
+ rewrite <- Ropp_mult_distr_l_reverse; rewrite scal_sum; 
+ apply sum_eq.
+intros; unfold sin_n, Un, tg_alt in |- *;
+ replace ((-1) ^ S i) with (- (-1) ^ i).
+replace (a ^ (2 * S i + 1)) with (Rsqr a * Rsqr a ^ i * a).
+unfold Rdiv in |- *; ring.
+rewrite pow_add; rewrite pow_Rsqr; simpl in |- *; ring.
+simpl in |- *; ring.
+unfold sin_n in |- *; unfold Rdiv in |- *; simpl in |- *; rewrite Rinv_1;
+ rewrite Rmult_1_r; reflexivity.
+apply lt_O_Sn.
+unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+assumption.
+apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption.
+unfold sin in |- *; case (exist_sin (Rsqr a)).
+intros; cut (x = x0).
+intro; rewrite H3; unfold Rdiv in |- *.
+symmetry  in |- *; apply Rinv_r_simpl_m; assumption.
+unfold sin_in in p; unfold sin_in in s; eapply uniqueness_sum.
+apply p.
+apply s.
+intros; elim H2; intros.
+replace (sin a - a) with (- (a - sin a)); [ idtac | ring ].
+split; apply Ropp_le_contravar; assumption.
+replace (- sum_f_R0 (tg_alt Un) (S (2 * n))) with
+ (-1 * sum_f_R0 (tg_alt Un) (S (2 * n))); [ rewrite scal_sum | ring ].
+apply sum_eq; intros; unfold sin_term, Un, tg_alt in |- *;
+ replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+unfold Rdiv in |- *; ring.
+reflexivity.
+replace (- sum_f_R0 (tg_alt Un) (2 * n)) with
+ (-1 * sum_f_R0 (tg_alt Un) (2 * n)); [ rewrite scal_sum | ring ].
+apply sum_eq; intros.
+unfold sin_term, Un, tg_alt in |- *;
+ replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+unfold Rdiv in |- *; ring.
+reflexivity.
+replace (2 * (n + 1))%nat with (S (S (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 (2 * n + 1)%nat with (S (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 Rplus_le_reg_l with (- a).
+rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
+ rewrite (Rplus_comm (- a)); apply H2.
+apply Rplus_le_reg_l with (- a).
+rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
+ rewrite (Rplus_comm (- a)); apply H3.
+unfold sin_term in |- *; simpl in |- *; unfold Rdiv in |- *; rewrite Rinv_1;
+ ring.
+replace (2 * (n + 1))%nat with (S (S (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 (2 * n + 1)%nat with (S (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  in |- *; assumption ].
 Qed.
 
 (**********)
-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 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)``.
-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``.
-Sup0.
-Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m.
-Replace ``2*2`` with ``4``; [Apply PI_4 | Ring].
-DiscrR.
-Assumption.
-Left; Sup0.
-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.
-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 unicity_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_sym; 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.
+Lemma cos_bound :
+ forall (a:R) (n:nat),
+   - PI / 2 <= a ->
+   a <= PI / 2 ->
+   cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1)). 
+cut
+ ((forall (a:R) (n:nat),
+     0 <= a ->
+     a <= PI / 2 ->
+     cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1))) ->
+  forall (a:R) (n:nat),
+    - PI / 2 <= a ->
+    a <= PI / 2 ->
+    cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1))).
+intros H a n; apply H.
+intros; unfold cos_approx in |- *.
+rewrite (decomp_sum (cos_term a0) (2 * n0 + 1)).
+rewrite (decomp_sum (cos_term a0) (2 * (n0 + 1))).
+replace (cos_term a0 0) with 1.
+cut
+ (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * n0 + 1)) <= cos a0 - 1 /\
+  cos a0 - 1 <=
+  sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * (n0 + 1))) ->
+  1 + sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * n0 + 1)) <= cos a0 /\
+  cos a0 <=
+  1 + sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * (n0 + 1)))).
+intro; apply H2.
+pose (Un := fun n:nat => a0 ^ (2 * S n) / INR (fact (2 * S n))).
+replace (pred (2 * n0 + 1)) with (2 * n0)%nat.
+replace (pred (2 * (n0 + 1))) with (S (2 * n0)).
+replace (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (2 * n0)) with
+ (- sum_f_R0 (tg_alt Un) (2 * n0)).
+replace (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (S (2 * n0))) with
+ (- sum_f_R0 (tg_alt Un) (S (2 * n0))).
+cut
+ (sum_f_R0 (tg_alt Un) (S (2 * n0)) <= 1 - cos a0 <=
+  sum_f_R0 (tg_alt Un) (2 * n0) ->
+  - sum_f_R0 (tg_alt Un) (2 * n0) <= cos a0 - 1 <=
+  - sum_f_R0 (tg_alt Un) (S (2 * n0))).
+intro; apply H3.
+apply alternated_series_ineq.
+unfold Un_decreasing in |- *; intro; unfold Un in |- *.
+cut ((2 * S (S n1))%nat = S (S (2 * S n1))).
+intro; rewrite H4;
+ replace (a0 ^ S (S (2 * S n1))) with (a0 ^ (2 * S n1) * (a0 * a0)).
+unfold Rdiv in |- *; rewrite Rmult_assoc; apply Rmult_le_compat_l.
+apply pow_le; assumption.
+apply Rmult_le_reg_l with (INR (fact (S (S (2 * S n1))))).
+rewrite <- H4; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
+ assert (H6 := sym_eq H5); elim (fact_neq_0 _ H6).
+rewrite <- H4; rewrite (Rmult_comm (INR (fact (2 * S (S n1)))));
+ rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_r; rewrite H4; do 2 rewrite fact_simpl; do 2 rewrite mult_INR;
+ repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
+rewrite Rmult_1_r; do 2 rewrite S_INR; rewrite mult_INR; repeat rewrite S_INR;
+ simpl in |- *;
+ 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 | ring_Rsqr ].
+replace (a0 * a0) with (Rsqr a0); [ idtac | reflexivity ].
+apply Rsqr_incr_1.
+apply Rle_trans with (PI / 2).
+assumption.
+unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
+prove_sup0.
+rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m.
+replace 4 with 4; [ apply PI_4 | ring ].
+discrR.
+assumption.
+left; prove_sup0.
+pattern 4 at 1 in |- *; rewrite <- Rplus_0_r; replace 12 with (4 + 8);
+ [ apply Rplus_le_compat_l; left; prove_sup0 | ring ].
+rewrite <- (Rplus_comm 12); pattern 12 at 1 in |- *; rewrite <- Rplus_0_r;
+ apply Rplus_le_compat_l.
+apply Rplus_le_le_0_compat.
+repeat apply Rmult_le_pos.
+left; prove_sup0.
+left; prove_sup0.
+replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+apply Rmult_le_pos.
+left; prove_sup0.
+replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+apply INR_fact_neq_0.
+apply INR_fact_neq_0.
+simpl in |- *; 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 in |- *; unfold Un_cv in H4;
+ unfold R_dist in H4; unfold Un_cv in |- *; unfold R_dist in |- *; 
+ intros; elim (H4 eps H5); intros N H6; exists N; intros.
+apply H6; unfold ge in |- *; apply le_trans with (2 * S N)%nat.
+apply le_trans with (2 * N)%nat.
+apply le_n_2n.
+apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_Sn.
+apply (fun m n p:nat => mult_le_compat_l p n m); 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 in |- *; unfold R_dist in |- *; 
+ intros.
+elim (p _ H5); intros N H6.
+exists N; intros.
+replace (sum_f_R0 (tg_alt Un) n1) with
+ (1 - sum_f_R0 (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)).
+unfold Rminus in |- *; rewrite Ropp_plus_distr; rewrite Ropp_involutive;
+ repeat rewrite Rplus_assoc; rewrite (Rplus_comm 1);
+ rewrite (Rplus_comm (-1)); repeat rewrite Rplus_assoc; 
+ rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite <- Rabs_Ropp;
+ rewrite Ropp_plus_distr; rewrite Ropp_involutive; 
+ unfold Rminus in H6; apply H6.
+unfold ge in |- *; apply le_trans with n1.
+exact H7.
+apply le_n_Sn.
+rewrite (decomp_sum (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)).
+replace (cos_n 0) with 1.
+simpl in |- *; rewrite Rmult_1_r; unfold Rminus in |- *;
+ rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; rewrite Rplus_opp_r;
+ rewrite Rplus_0_l;
+ replace (- sum_f_R0 (fun i:nat => cos_n (S i) * (Rsqr a0 * Rsqr a0 ^ i)) n1)
+  with
+  (-1 * sum_f_R0 (fun i:nat => cos_n (S i) * (Rsqr a0 * Rsqr a0 ^ i)) n1);
+ [ idtac | ring ]; rewrite scal_sum; apply sum_eq; 
+ intros; unfold cos_n, Un, tg_alt in |- *.
+replace ((-1) ^ S i) with (- (-1) ^ i).
+replace (a0 ^ (2 * S i)) with (Rsqr a0 * Rsqr a0 ^ i).
+unfold Rdiv in |- *; ring.
+rewrite pow_Rsqr; reflexivity.
+simpl in |- *; ring.
+unfold cos_n in |- *; unfold Rdiv in |- *; simpl in |- *; rewrite Rinv_1;
+ rewrite Rmult_1_r; reflexivity.
+apply lt_O_Sn.
+unfold cos in |- *; case (exist_cos (Rsqr a0)); intros; unfold cos_in in p;
+ unfold cos_in in c; eapply uniqueness_sum.
+apply p.
+apply c.
+intros; elim H3; intros; replace (cos a0 - 1) with (- (1 - cos a0));
+ [ idtac | ring ].
+split; apply Ropp_le_contravar; assumption.
+replace (- sum_f_R0 (tg_alt Un) (S (2 * n0))) with
+ (-1 * sum_f_R0 (tg_alt Un) (S (2 * n0))); [ rewrite scal_sum | ring ].
+apply sum_eq; intros; unfold cos_term, Un, tg_alt in |- *;
+ replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+unfold Rdiv in |- *; ring.
+reflexivity.
+replace (- sum_f_R0 (tg_alt Un) (2 * n0)) with
+ (-1 * sum_f_R0 (tg_alt Un) (2 * n0)); [ rewrite scal_sum | ring ];
+ apply sum_eq; intros; unfold cos_term, Un, tg_alt in |- *;
+ replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+unfold Rdiv in |- *; ring.
+reflexivity.
+replace (2 * (n0 + 1))%nat with (S (S (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 (2 * n0 + 1)%nat with (S (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 Rplus_le_reg_l with (-1).
+rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
+ rewrite (Rplus_comm (-1)); apply H3.
+apply Rplus_le_reg_l with (-1).
+rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
+ rewrite (Rplus_comm (-1)); apply H4.
+unfold cos_term in |- *; simpl in |- *; unfold Rdiv in |- *; rewrite Rinv_1;
+ ring.
+replace (2 * (n0 + 1))%nat with (S (S (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 (2 * n0 + 1)%nat with (S (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 0 a); intro.
+elim s; intro.
+apply H; [ left; assumption | assumption ].
+apply H; [ right; assumption | assumption ].
+cut (0 < - a).
+intro; cut (forall (x:R) (n:nat), cos_approx x n = cos_approx (- x) n).
+intro; rewrite H3; rewrite (H3 a (2 * (n + 1))%nat); rewrite cos_sym; apply H.
+left; assumption.
+rewrite <- (Ropp_involutive (PI / 2)); apply Ropp_le_contravar;
+ unfold Rdiv in |- *; unfold Rdiv in H0; rewrite <- Ropp_mult_distr_l_reverse;
+ exact H0.
+intros; unfold cos_approx in |- *; apply sum_eq; intros;
+ unfold cos_term in |- *; do 2 rewrite pow_Rsqr; rewrite Rsqr_neg;
+ unfold Rdiv in |- *; reflexivity.
+apply Ropp_0_gt_lt_contravar; assumption.
+Qed.
\ No newline at end of file