Library Coq.Reals.Rtrigo_calc

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo1.
Require Import R_sqrt.
Local Open Scope R_scope.

Lemma tan_PI : tan PI = 0.

Lemma sin_3PI2 : sin (3 * (PI / 2)) = -1.

Lemma tan_2PI : tan (2 * PI) = 0.

Lemma sin_cos_PI4 : sin (PI / 4) = cos (PI / 4).

Lemma sin_PI3_cos_PI6 : sin (PI / 3) = cos (PI / 6).

Lemma sin_PI6_cos_PI3 : cos (PI / 3) = sin (PI / 6).

Lemma PI6_RGT_0 : 0 < PI / 6.

Lemma PI6_RLT_PI2 : PI / 6 < PI / 2.

Lemma sin_PI6 : sin (PI / 6) = 1 / 2.

Lemma sqrt2_neq_0 : sqrt 2 <> 0.

Lemma R1_sqrt2_neq_0 : 1 / sqrt 2 <> 0.

Lemma sqrt3_2_neq_0 : 2 * sqrt 3 <> 0.

Lemma Rlt_sqrt2_0 : 0 < sqrt 2.

Lemma Rlt_sqrt3_0 : 0 < sqrt 3.

Lemma PI4_RGT_0 : 0 < PI / 4.

Lemma cos_PI4 : cos (PI / 4) = 1 / sqrt 2.

Lemma sin_PI4 : sin (PI / 4) = 1 / sqrt 2.

Lemma tan_PI4 : tan (PI / 4) = 1.

Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.

Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2.

Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2.

Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3.

Lemma sin_PI3 : sin (PI / 3) = sqrt 3 / 2.

Lemma cos_PI3 : cos (PI / 3) = 1 / 2.

Lemma tan_PI3 : tan (PI / 3) = sqrt 3.

Lemma sin_2PI3 : sin (2 * (PI / 3)) = sqrt 3 / 2.

Lemma cos_2PI3 : cos (2 * (PI / 3)) = -1 / 2.

Lemma tan_2PI3 : tan (2 * (PI / 3)) = - sqrt 3.

Lemma cos_5PI4 : cos (5 * (PI / 4)) = -1 / sqrt 2.

Lemma sin_5PI4 : sin (5 * (PI / 4)) = -1 / sqrt 2.

Lemma sin_cos5PI4 : cos (5 * (PI / 4)) = sin (5 * (PI / 4)).

Lemma Rgt_3PI2_0 : 0 < 3 * (PI / 2).

Lemma Rgt_2PI_0 : 0 < 2 * PI.

Lemma Rlt_PI_3PI2 : PI < 3 * (PI / 2).

Lemma Rlt_3PI2_2PI : 3 * (PI / 2) < 2 * PI.

Definition plat : R := 180.
Definition toRad (x:R) : R := x * PI * / plat.
Definition toDeg (x:R) : R := x * plat * / PI.

Lemma rad_deg : forall x:R, toRad (toDeg x) = x.

Lemma toRad_inj : forall x y:R, toRad x = toRad y -> x = y.

Lemma deg_rad : forall x:R, toDeg (toRad x) = x.

Definition sind (x:R) : R := sin (toRad x).
Definition cosd (x:R) : R := cos (toRad x).
Definition tand (x:R) : R := tan (toRad x).

Lemma Rsqr_sin_cos_d_one : forall x:R, Rsqr (sind x) + Rsqr (cosd x) = 1.

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