From 855cc609d2888ef59d848ed688f02390811b28c7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 29 Feb 2008 18:55:04 +0000
Subject: Argumentation plus poussée de pourquoi on retire la condition x>0
 dans Rpower_O alors qu'on la garde pour les autres propriétés de la
 puissance. (résultat d'une discussion avec Assia et Jean-Marc)

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

diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 61cd98e56b..701ed449b0 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -403,6 +403,9 @@ 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" *)
+
 Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y.
 Proof.
   intros x y z; unfold Rpower in |- *.
-- 
cgit v1.2.3