diff -r 6c52b1d71f8b -r d8fb621fea02 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Feb 10 23:04:45 2020 +0100
+++ b/src/HOL/Power.thy	Tue Feb 11 12:55:35 2020 +0000
@@ -904,13 +904,14 @@
   from power_strict_increasing_iff [OF this] less show ?thesis ..
 qed
 
-lemma power_dvd_imp_le: "i ^ m dvd i ^ n \<Longrightarrow> 1 < i \<Longrightarrow> m \<le> n"
-  for i m n :: nat
-  apply (rule power_le_imp_le_exp)
-   apply assumption
-  apply (erule dvd_imp_le)
-  apply simp
-  done
+lemma power_gt_expt: "n > Suc 0 \<Longrightarrow> n^k > k"
+  by (induction k) (auto simp: less_trans_Suc n_less_m_mult_n)
+
+lemma power_dvd_imp_le:
+  fixes i :: nat
+  assumes "i ^ m dvd i ^ n" "1 < i"
+  shows "m \<le> n"
+  using assms by (auto intro: power_le_imp_le_exp [OF \<open>1 < i\<close> dvd_imp_le])
 
 lemma dvd_power_iff_le:
   fixes k::nat
@@ -968,7 +969,7 @@
 qed
 
 lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2"
-shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
+  shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
 proof -
   have "1 \<le> k - 1" using assms(2) by arith
   from ex_power_ivl1[OF assms(1) this]