From dc71c8b582552dcc1ea40af8a2894f7f0ec84597 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 6 Sep 2017 13:01:23 +0200 Subject: weakens an hypothesis of Rle_Rpower --- theories/Reals/Rpower.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'theories') 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. -- cgit v1.2.3