src/HOL/Power.thy

--- a/src/HOL/Power.thy	Wed Oct 28 12:21:38 2009 +0000
+++ b/src/HOL/Power.thy	Wed Oct 28 17:44:03 2009 +0100
@@ -452,6 +452,12 @@
   from power_strict_increasing_iff [OF this] less show ?thesis ..
 qed
 
+lemma power_dvd_imp_le:
+  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
+  apply (rule power_le_imp_le_exp, assumption)
+  apply (erule dvd_imp_le, simp)
+  done
+
 
 subsection {* Code generator tweak *}