# 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 cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.

#[deprecated(since="8.10",note="Use cos_3PI4 instead.")] Notation cos3PI4 := cos_3PI4.

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

#[deprecated(since="8.10",note="Use sin_3PI4 instead.")] Notation sin3PI4 := sin_3PI4.

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.