4 files changed, 23 insertions, 13 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index ddf2d4ebf..59a104965 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1613,6 +1613,9 @@ Proof.
 Qed.
 Hint Resolve mult_INR: real.
 
+Lemma pow_INR (m n: nat) :  INR (m ^ n) = pow (INR m) n.
+Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed.
+
 (*********)
 Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
 Proof.
@@ -2026,7 +2029,7 @@ Qed.
 
 Lemma R_rm : ring_morph
   0%R 1%R Rplus Rmult Rminus Ropp eq
-  0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR.
+  0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR.
 Proof.
 constructor ; try easy.
 exact plus_IZR.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index bceb4a6cd..aa886cee0 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -611,7 +611,7 @@ Qed.
 
 Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z).
 Proof.
-  intros z; case z; unfold Zabs.
+  intros z; case z; unfold Z.abs.
   apply Rabs_R0.
   now intros p0; apply Rabs_pos_eq, (IZR_le 0).
   unfold IZR at 1.
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 59604516f..04f13477c 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -65,7 +65,7 @@ destruct (Rle_lt_dec l 0) as [Hl|Hl].
   now apply Rinv_0_lt_compat.
   now apply Hnp.
 left.
-set (N := Zabs_nat (up (/l) - 2)).
+set (N := Z.abs_nat (up (/l) - 2)).
 assert (H1l: (1 <= /l)%R).
   rewrite <- Rinv_1.
   apply Rinv_le_contravar with (1 := Hl).
@@ -77,7 +77,7 @@ assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R).
   rewrite inj_Zabs_nat.
   replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R.
   apply (f_equal (fun v => IZR v + 1)%R).
-  apply Zabs_eq.
+  apply Z.abs_eq.
   apply Zle_minus_le_0.
   apply (Zlt_le_succ 1).
   apply lt_IZR.
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index ae2e7772b..c6fac951b 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -433,9 +433,9 @@ Proof.
 Qed.
 
 Theorem Rpower_lt :
-  forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z.
+  forall x y z:R, 1 < x -> y < z -> x ^R y < x ^R z.
 Proof.
-  intros x y z H H0 H1.
+  intros x y z H H1.
   unfold Rpower.
   apply exp_increasing.
   apply Rmult_lt_compat_r.
@@ -490,11 +490,13 @@ Proof.
 Qed.
 
 Theorem Rle_Rpower :
-  forall e n m:R, 1 < e -> 0 <= n -> 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 H0 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.
@@ -709,13 +711,18 @@ intros x y z x0 y0; unfold Rpower.
 rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto.
 Qed.
 
-Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c. 
+Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c.
+Proof.
+intros c0 [a0 ab]; apply exp_increasing.
+now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier.
+Qed.
+
+Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c.
 Proof.
 intros [c0 | c0];
  [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ].
   intros [a0 [ab|ab]].
-   left; apply exp_increasing.
-   now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier.
+  now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier.
   rewrite ab; apply Rle_refl.
  apply Rlt_le_trans with a; tauto.
 tauto.