src/HOL/Power.thy

--- a/src/HOL/Power.thy	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/HOL/Power.thy	Thu Sep 12 14:51:45 2019 +0100
@@ -895,6 +895,11 @@
   apply simp
   done
 
+lemma dvd_power_iff_le:
+  fixes k::nat
+  shows "2 \<le> k \<Longrightarrow> ((k ^ m) dvd (k ^ n) \<longleftrightarrow> m \<le> n)"
+  using le_imp_power_dvd power_dvd_imp_le by force
+
 lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
   for m n :: nat
   by (auto intro: power2_le_imp_le power_mono)