diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-01 14:00:22 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-01 14:00:22 +0000 |
| commit | 6e67224b7b953d94985fc3e307321b37d072ffad (patch) | |
| tree | f24fa4cfedf3ae2b4c4dbd1186d674e82251afb8 /theories/Reals/Rtrigo_def.v | |
| parent | 672bf2669fff6131ade8ed21310e1dd25e30e65d (diff) | |
PI n'est plus un axiome
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2818 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_def.v')
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index b1377776d..5b9422c59 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -15,6 +15,7 @@ Require Rbase. Require Rseries. Require Rtrigo_fun. Require Export Alembert. +Require Export AltSeries. (*****************************) (* Definition of exponential *) @@ -368,17 +369,7 @@ Intro; Unfold sin; Replace ``(Rsqr (-x))`` with (Rsqr x); [Idtac | Apply Rsqr_ne Case (exist_sin (Rsqr x)); Intros; Ring. Qed. -Axiom PI_ax : (SigT R [l:R]``0<l``/\``(sin (l/2))==1``/\((l1:R)``0<l1``->``(sin (l1/2))==1``->``l<=l1``)). - -(**********) -Definition PI : R := (projT1 ? ? PI_ax). - (**********) -Lemma PI_RGT_0 : ``0<PI``. -Assert X := (projT2 ? ? PI_ax). -Elim X; Intros; Unfold PI; Exact H. -Qed. - Axiom sin_plus : (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)``. @@ -425,6 +416,4 @@ Exact (projT2 ? ? exist_cos0). Assert H := (projT2 ? ? (exist_cos (Rsqr R0))); Unfold cos; Pattern 1 R0; Replace R0 with (Rsqr R0); [Exact H | Apply Rsqr_O]. Qed. -Lemma sin_PI2 : ``(sin (PI/2))==1``. -Assert H := (projT2 ? ? PI_ax); Elim H; Intros; Elim H1; Intros; Unfold PI; Exact H2. -Qed. +Axiom sin_PI2 : ``(sin (PI/2))==1``. |