diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 12:33:41 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 12:33:41 +0000 |
| commit | e52b55b2e60a38f61b0fd6b161e081e825bcf8be (patch) | |
| tree | 0b6f49c85b8e76add1a331c4c3d15dd1305ba52d /theories | |
| parent | 3f054c565ffed6356e3eaea15495eebf637ef126 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2269 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -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))``. |