The Coq Proof Assistant

# Library Coq.Reals.Rtrigo_alt

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo_def.
Require Import Lia Lra.
Local Open 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.
Theorem pre_sin_bound :
forall (a:R) (n:nat),
0 <= a ->
a <= 4 -> sin_approx a (2 * n + 1) <= sin a <= sin_approx a (2 * (n + 1)).
Lemma pre_cos_bound :
forall (a:R) (n:nat),
- 2 <= a -> a <= 2 ->
cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1)).