diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-01 16:26:18 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-01 16:26:18 +0000 |
commit | 6671de91bd93189bbfa330fffaba8890177661fe (patch) | |
tree | acf08a49e84f19b0e6221349593b45fc4f426d47 /theories/Reals/Rpower.v | |
parent | 0d62e3344d7f69c0296c347c7aeddabd09bbab60 (diff) |
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
Diffstat (limited to 'theories/Reals/Rpower.v')
-rw-r--r-- | theories/Reals/Rpower.v | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 701ed449b..f254019c7 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. |