From e52b55b2e60a38f61b0fd6b161e081e825bcf8be Mon Sep 17 00:00:00 2001 From: desmettr Date: Wed, 5 Dec 2001 12:33:41 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2269 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rtrigo.v | 8 ++++++-- 1 file 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)``. @@ -38,6 +36,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)``. -- cgit v1.2.3