# Library Coq.Reals.Rtrigo_alt

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) (i:nat) : R :=
(-1) ^ i * ( a ^ (2 * i + 1) / INR (fact (2 * i + 1))).
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 cos_approx (a:R) (n:nat) : R := sum_f_R0 (cos_term a) n.
Lemma PI_4 : PI <= 4.
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)).
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)).