diff options
Diffstat (limited to 'theories')
| -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. |