From 3d4c856d295fba4015ccb92bfb8da7f08f3679e5 Mon Sep 17 00:00:00 2001 From: desmettr Date: Mon, 17 Jun 2002 13:54:54 +0000 Subject: Modifications relatives a l'ajout de Rtrigo_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2790 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rtrigo.v | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index e2cdb2434c..06222a5d30 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -15,11 +15,7 @@ Require Rbase. Require R_sqr. Require Rfunctions. Require Rsigma. - -(**********) -Parameter PI : R. - -Axiom PI_RGT_0 : ``0R. -Parameter cos : R->R. - -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)``. - -Axiom cos_plus : (x,y:R) ``(cos (x+y))==(cos x)*(cos y)-(sin x)*(sin y)``. - -Axiom cos_minus : (x,y:R) ``(cos (x-y))==(cos x)*(cos y)+(sin x)*(sin y)``. - -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. -- cgit v1.2.3