diff options
| -rw-r--r-- | theories/Reals/Rtrigo.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index fa07efe98..bc7892207 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -24,8 +24,6 @@ Save. Parameter sin : R->R. Parameter cos : R->R. -Axiom sin2_cos2 : (x:R) ``(Rsqr (sin x)) + (Rsqr (cos x))==1``. - Axiom sin_plus : (x,y:R) ``(sin (x+y))==(sin x)*(cos y)+(cos x)*(sin y)``. Axiom sin_minus : (x,y:R) ``(sin (x-y))==(sin x)*(cos y)-(cos x)*(sin y)``. @@ -39,6 +37,12 @@ Axiom cos_0 : ``(cos 0)==1``. Axiom sin_PI2 : ``(sin (PI/2))==1``. (**********) +Lemma sin2_cos2 : (x:R) ``(Rsqr (sin x)) + (Rsqr (cos x))==1``. +Intro; Unfold Rsqr; Rewrite Rplus_sym; Rewrite <- (cos_minus x x); Unfold Rminus; Rewrite Rplus_Ropp_r; Apply cos_0. +Save. + + +(**********) Definition tan [x:R] : R := ``(sin x)/(cos x)``. Lemma tan_plus : (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))``. |