diff options
| -rw-r--r-- | theories/Reals/Rpower.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index ddf7f568e..301fe20b0 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -488,11 +488,13 @@ Proof. Qed. Theorem Rle_Rpower : - forall e n m:R, 1 < e -> n <= m -> e ^R n <= e ^R m. + forall e n m:R, 1 <= e -> n <= m -> e ^R n <= e ^R m. Proof. - intros e n m H H1; case H1. - intros H2; left; apply Rpower_lt; assumption. - intros H2; rewrite H2; right; reflexivity. + intros e n m [H | H]; intros H1. + case H1. + intros H2; left; apply Rpower_lt; assumption. + intros H2; rewrite H2; right; reflexivity. + now rewrite <- H; unfold Rpower; rewrite ln_1, !Rmult_0_r; apply Rle_refl. Qed. Theorem ln_lt_2 : / 2 < ln 2. |