Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Export Rtrigo_fun.
Require Export Rtrigo_def.
Require Export Rtrigo_alt.
Require Export Cos_rel.
Require Export Cos_plus.
Require Import ZArith_base.
Require Import Zcomplements.
Require Import Lra.
Require Import Ranalysis1.
Require Import Rsqrt_def.
Require Import PSeries_reg.

Local Open Scope nat_scope.
Local Open Scope R_scope.

Lemma CVN_R_cos :
  forall fn:nat -> R -> R,
    fn = (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)) ->
    CVN_R fn.

Lemma continuity_cos : continuity cos.

Lemma sin_gt_cos_7_8 : sin (7 / 8) > cos (7 / 8).

Definition PI_2_aux : {z | 7/8 <= z <= 7/4 /\ -cos z = 0}.
Qed.

Definition PI2 := proj1_sig PI_2_aux.

Definition PI := 2 * PI2.

Lemma cos_pi2 : cos PI2 = 0.

Lemma pi2_int : 7/8 <= PI2 <= 7/4.

Lemma cos_minus : forall x y:R, cos (x - y) = cos x * cos y + sin x * sin y.

Lemma sin2_cos2 : forall x:R, Rsqr (sin x) + Rsqr (cos x) = 1.

Lemma cos2 : forall x:R, Rsqr (cos x) = 1 - Rsqr (sin x).

Lemma sin2 : forall x:R, Rsqr (sin x) = 1 - Rsqr (cos x).

Lemma cos_PI2 : cos (PI / 2) = 0.

Lemma sin_pos_tech : forall x, 0 < x < 2 -> 0 < sin x.

Lemma sin_PI2 : sin (PI / 2) = 1.

Lemma PI_RGT_0 : PI > 0.

Lemma PI_4 : PI <= 4.

Lemma PI_neq0 : PI <> 0.

Lemma cos_PI : cos PI = -1.

Lemma sin_PI : sin PI = 0.

Lemma 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)).
Lemma neg_cos : forall x:R, cos (x + PI) = - cos x.

Lemma sin_cos : forall x:R, sin x = - cos (PI / 2 + x).

Lemma sin_plus : forall x y:R, sin (x + y) = sin x * cos y + cos x * sin y.

Lemma sin_minus : forall x y:R, sin (x - y) = sin x * cos y - cos x * sin y.

Definition tan (x:R) : R := sin x / cos x.

Lemma tan_plus :
  forall x y:R,
    cos x <> 0 ->
    cos y <> 0 ->
    cos (x + y) <> 0 ->
    1 - tan x * tan y <> 0 ->
    tan (x + y) = (tan x + tan y) / (1 - tan x * tan y).

Lemma sin_2a : forall x:R, sin (2 * x) = 2 * sin x * cos x.

Lemma cos_2a : forall x:R, cos (2 * x) = cos x * cos x - sin x * sin x.

Lemma cos_2a_cos : forall x:R, cos (2 * x) = 2 * cos x * cos x - 1.

Lemma cos_2a_sin : forall x:R, cos (2 * x) = 1 - 2 * sin x * sin x.

Lemma tan_2a :
  forall x:R,
    cos x <> 0 ->
    cos (2 * x) <> 0 ->
    1 - tan x * tan x <> 0 -> tan (2 * x) = 2 * tan x / (1 - tan x * tan x).

Lemma sin_neg : forall x:R, sin (- x) = - sin x.

Lemma cos_neg : forall x:R, cos (- x) = cos x.

Lemma tan_0 : tan 0 = 0.

Lemma tan_neg : forall x:R, tan (- x) = - tan x.

Lemma tan_minus :
  forall x y:R,
    cos x <> 0 ->
    cos y <> 0 ->
    cos (x - y) <> 0 ->
    1 + tan x * tan y <> 0 ->
    tan (x - y) = (tan x - tan y) / (1 + tan x * tan y).

Lemma cos_3PI2 : cos (3 * (PI / 2)) = 0.

Lemma sin_2PI : sin (2 * PI) = 0.

Lemma cos_2PI : cos (2 * PI) = 1.

Lemma neg_sin : forall x:R, sin (x + PI) = - sin x.

Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x.

Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x.

Lemma cos_period : forall (x:R) (k:nat), cos (x + 2 * INR k * PI) = cos x.

Lemma sin_shift : forall x:R, sin (PI / 2 - x) = cos x.

Lemma cos_shift : forall x:R, cos (PI / 2 - x) = sin x.

Lemma cos_sin : forall x:R, cos x = sin (PI / 2 + x).

Lemma PI2_RGT_0 : 0 < PI / 2.

Lemma SIN_bound : forall x:R, -1 <= sin x <= 1.

Lemma COS_bound : forall x:R, -1 <= cos x <= 1.

Lemma cos_sin_0 : forall x:R, ~ (cos x = 0 /\ sin x = 0).

Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0.

Definition sin_lb (a:R) : R := sin_approx a 3.
Definition sin_ub (a:R) : R := sin_approx a 4.
Definition cos_lb (a:R) : R := cos_approx a 3.
Definition cos_ub (a:R) : R := cos_approx a 4.

Lemma sin_lb_gt_0 : forall a:R, 0 < a -> a <= PI / 2 -> 0 < sin_lb a.

Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.

Lemma COS :
  forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a.

Lemma _PI2_RLT_0 : - (PI / 2) < 0.

Lemma PI4_RLT_PI2 : PI / 4 < PI / 2.

Lemma PI2_Rlt_PI : PI / 2 < PI.

Theorem sin_gt_0 : forall x:R, 0 < x -> x < PI -> 0 < sin x.

Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x.

Lemma sin_ge_0 : forall x:R, 0 <= x -> x <= PI -> 0 <= sin x.

Lemma cos_ge_0 : forall x:R, - (PI / 2) <= x -> x <= PI / 2 -> 0 <= cos x.

Lemma sin_le_0 : forall x:R, PI <= x -> x <= 2 * PI -> sin x <= 0.

Lemma cos_le_0 : forall x:R, PI / 2 <= x -> x <= 3 * (PI / 2) -> cos x <= 0.

Lemma sin_lt_0 : forall x:R, PI < x -> x < 2 * PI -> sin x < 0.

Lemma sin_lt_0_var : forall x:R, - PI < x -> x < 0 -> sin x < 0.

Lemma cos_lt_0 : forall x:R, PI / 2 < x -> x < 3 * (PI / 2) -> cos x < 0.

Lemma tan_gt_0 : forall x:R, 0 < x -> x < PI / 2 -> 0 < tan x.

Lemma tan_lt_0 : forall x:R, - (PI / 2) < x -> x < 0 -> tan x < 0.

Lemma cos_ge_0_3PI2 :
  forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x.

Lemma form1 :
  forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2).

Lemma form2 :
  forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2).

Lemma form3 :
  forall p q:R, sin p + sin q = 2 * cos ((p - q) / 2) * sin ((p + q) / 2).

Lemma form4 :
  forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2).

Lemma sin_increasing_0 :
  forall x y:R,
    - (PI / 2) <= x ->
    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> sin x < sin y -> x < y.

Lemma sin_increasing_1 :
  forall x y:R,
    - (PI / 2) <= x ->
    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> x < y -> sin x < sin y.

Lemma sin_decreasing_0 :
  forall x y:R,
    x <= 3 * (PI / 2) ->
    PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> sin x < sin y -> y < x.

Lemma sin_decreasing_1 :
  forall x y:R,
    x <= 3 * (PI / 2) ->
    PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> x < y -> sin y < sin x.

Lemma cos_increasing_0 :
  forall x y:R,
    PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x < cos y -> x < y.

Lemma cos_increasing_1 :
  forall x y:R,
    PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x < y -> cos x < cos y.

Lemma cos_decreasing_0 :
  forall x y:R,
    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x < cos y -> y < x.

Lemma cos_decreasing_1 :
  forall x y:R,
    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x < y -> cos y < cos x.

Lemma tan_diff :
  forall x y:R,
    cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y).

Lemma tan_increasing_0 :
  forall x y:R,
    - (PI / 4) <= x ->
    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> tan x < tan y -> x < y.

Lemma tan_increasing_1 :
  forall x y:R,
    - (PI / 4) <= x ->
    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> x < y -> tan x < tan y.

Lemma sin_incr_0 :
  forall x y:R,
    - (PI / 2) <= x ->
    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> sin x <= sin y -> x <= y.

Lemma sin_incr_1 :
  forall x y:R,
    - (PI / 2) <= x ->
    x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> x <= y -> sin x <= sin y.

Lemma sin_decr_0 :
  forall x y:R,
    x <= 3 * (PI / 2) ->
    PI / 2 <= x ->
    y <= 3 * (PI / 2) -> PI / 2 <= y -> sin x <= sin y -> y <= x.

Lemma sin_decr_1 :
  forall x y:R,
    x <= 3 * (PI / 2) ->
    PI / 2 <= x ->
    y <= 3 * (PI / 2) -> PI / 2 <= y -> x <= y -> sin y <= sin x.

Lemma cos_incr_0 :
  forall x y:R,
    PI <= x ->
    x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x <= cos y -> x <= y.

Lemma cos_incr_1 :
  forall x y:R,
    PI <= x ->
    x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x <= y -> cos x <= cos y.

Lemma cos_decr_0 :
  forall x y:R,
    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x <= cos y -> y <= x.

Lemma cos_decr_1 :
  forall x y:R,
    0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x <= y -> cos y <= cos x.

Lemma tan_incr_0 :
  forall x y:R,
    - (PI / 4) <= x ->
    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> tan x <= tan y -> x <= y.

Lemma tan_incr_1 :
  forall x y:R,
    - (PI / 4) <= x ->
    x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> x <= y -> tan x <= tan y.

Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0.

Lemma sin_eq_0_0 (x:R) : sin x = 0 -> exists k : Z, x = IZR k * PI.

Lemma cos_eq_0_0 (x:R) :
  cos x = 0 -> exists k : Z, x = IZR k * PI + PI / 2.

Lemma cos_eq_0_1 (x:R) :
  (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0.

Lemma sin_eq_O_2PI_0 (x:R) :
  0 <= x -> x <= 2 * PI -> sin x = 0 ->
  x = 0 \/ x = PI \/ x = 2 * PI.

Lemma sin_eq_O_2PI_1 (x:R) :
  0 <= x -> x <= 2 * PI ->
  x = 0 \/ x = PI \/ x = 2 * PI -> sin x = 0.

Lemma cos_eq_0_2PI_0 (x:R) :
  0 <= x -> x <= 2 * PI -> cos x = 0 ->
  x = PI / 2 \/ x = 3 * (PI / 2).

Lemma cos_eq_0_2PI_1 (x:R) :
  0 <= x -> x <= 2 * PI ->
  x = PI / 2 \/ x = 3 * (PI / 2) -> cos x = 0.