diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-17 13:54:54 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-17 13:54:54 +0000 |
| commit | 3d4c856d295fba4015ccb92bfb8da7f08f3679e5 (patch) | |
| tree | 592002c0f44a869a039e550cbac459096dd5343b /theories/Reals/Rtrigo.v | |
| parent | f9125341b9e82f4a7658d4492c187b4057eb408b (diff) | |
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
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 25 |
1 files changed, 1 insertions, 24 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index e2cdb2434..06222a5d3 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 : ``0<PI``. +Require Export Rtrigo_def. Lemma PI_neq0 : ~``PI==0``. Red; Intro. @@ -27,25 +23,6 @@ Generalize PI_RGT_0; Intro; Rewrite H in H0. Elim (Rlt_antirefl ``0`` H0). Qed. -(******************************************************************) -(* Axiomatic definitions of cos and sin *) -(******************************************************************) - -Parameter sin : R->R. -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. |