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.

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)).