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.
Lemma sin_3PI4 : 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.
Radian -> Degree | Degree -> Radian
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.
Other properties