1 files changed, 4 insertions, 24 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index b3ce6fa33..f62ed2a6c 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -55,25 +55,8 @@ Proof.
     simpl in H0.
   replace (/ 3) with
   (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 +
-    -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)).
+    -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)) by field.
   apply H0.
-  repeat rewrite Rinv_1; repeat rewrite Rmult_1_r;
-    rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l;
-      rewrite Ropp_involutive; rewrite Rplus_opp_r; rewrite Rmult_1_r;
-        rewrite Rplus_0_l; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 6.
-  rewrite Rmult_plus_distr_l; replace (2 + 1 + 1 + 1 + 1) with 6.
-  rewrite <- (Rmult_comm (/ 6)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_l; replace 6 with 6.
-  do 2 rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_r; rewrite (Rmult_comm 3); rewrite <- Rmult_assoc;
-    rewrite <- Rinv_r_sym.
-  ring.
-  discrR.
-  discrR.
-  ring.
-  discrR.
-  ring.
-  discrR.
   apply H.
   unfold Un_decreasing; intros;
     apply Rmult_le_reg_l with (INR (fact n)).
@@ -505,12 +488,9 @@ Proof.
   rewrite Rinv_r.
   apply exp_lt_inv.
   apply Rle_lt_trans with (1 := exp_le_3).
-  change (3 < 2 ^R 2).
+  change (3 < 2 ^R (1 + 1)).
   repeat rewrite Rpower_plus; repeat rewrite Rpower_1.
-  repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
-    repeat rewrite Rmult_1_l.
-  pattern 3 at 1; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1);
-    [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ].
+  now apply (IZR_lt 3 4).
   prove_sup0.
   discrR.
 Qed.
@@ -732,7 +712,7 @@ Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)).
 Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x.
 intros x; unfold sinh, arcsinh.
 assert (Rminus_eq_0 : forall r, r - r = 0) by (intros; ring).
-pattern 1 at 5; rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus.
+rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus.
 rewrite exp_plus.
 match goal with |- context[sqrt ?a] => 
   replace a with (((exp x + exp(-x))/2)^2) by field