From 6e67224b7b953d94985fc3e307321b37d072ffad Mon Sep 17 00:00:00 2001
From: desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 1 Jul 2002 14:00:22 +0000
Subject: PI n'est plus un axiome

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2818 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rtrigo_def.v | 15 ++-------------
 1 file changed, 2 insertions(+), 13 deletions(-)

(limited to 'theories/Reals/Rtrigo_def.v')

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``.
-- 
cgit v1.2.3