diff options
| author |  Yves Bertot <Yves.Bertot@inria.fr> | 2017-09-06 13:01:23 +0200 |
|---|---|---|
| committer | Yves Bertot <Yves.Bertot@inria.fr> | 2017-09-06 13:01:23 +0200 |
| commit | dc71c8b582552dcc1ea40af8a2894f7f0ec84597 (patch) | |
| tree | 9897d66d8e6e9bf666e555d1a5240df7f6e759d8 /theories | |
| parent | 2d137819572c4307b34bfdbdcf4ad0dc9ab240f3 (diff) | |
weakens an hypothesis of Rle_Rpower
Diffstat (limited to 'theories')
| -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. |