diff options
| -rw-r--r-- | theories/Reals/Rpower.v | 3 |
1 files changed, 3 insertions, 0 deletions
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 |- *. |