From 684de856ad6c374d4f957f1897d0ae1d31b3b0f9 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Fri, 12 Jul 2002 11:57:39 +0000
Subject: cos_plus prouve

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

diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 44a020d570..92accec1cf 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -20,10 +20,9 @@ Require Rlimit.
 Require Binome.
 Require Export Rtrigo_def.
 Require Export Rtrigo_alt.
+Require Export Cos_plus.
 
-(* The two remaining axioms *)
-Axiom cos_plus : (x,y:R) ``(cos (x+y))==(cos x)*(cos y)-(sin x)*(sin y)``.
-
+(** sin_PI2 is the only remaining axiom **)
 Axiom sin_PI2 : ``(sin (PI/2))==1``.
 
 (* Here, we have the euclidian division *)
-- 
cgit v1.2.3