From 6671de91bd93189bbfa330fffaba8890177661fe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Mar 2008 16:26:18 +0000
Subject: Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_O
 (rapport de bug 1807). Cf explication dans le fichier et/ou dans le
 bug-tracker.

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

diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 701ed449b0..f254019c7d 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -403,8 +403,15 @@ Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
 (** *                     Properties of  Rpower                   *)
 (******************************************************************)
 
-(** Note: Because [ln] is artificially prolongated to 1 on negative
-    reals, no side condition is needed to state "x ^R 0 = 1" *)
+(** Note: [Rpower] is prolongated to [1] on negative real numbers and
+    it thus does not extend integer power. The next two lemmas, which
+    hold for integer power, accidentally hold on negative real numbers
+    as a side effect of the default value taken on negative real
+    numbers. Contrastingly, the lemmas that do not hold for the
+    integer power of a negative number are stated for [Rpower] on the
+    positive numbers only (even if they accidentally hold due to the
+    default value of [Rpower] on the negative side, as it is the case
+    for [Rpower_O]). *)
 
 Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y.
 Proof.
@@ -421,9 +428,9 @@ Proof.
   ring.
 Qed.
 
-Theorem Rpower_O : forall x:R, x ^R 0 = 1.
+Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1.
 Proof.
-  intros x; unfold Rpower in |- *.
+  intros x _; unfold Rpower in |- *.
   rewrite Rmult_0_l; apply exp_0.
 Qed.
 
-- 
cgit v1.2.3