src/HOL/Power.thy

   "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
 
+lemma power2_nat_le_eq_le:
+  fixes m n :: nat
+  shows "m\<twosuperior> \<le> n\<twosuperior> \<longleftrightarrow> m \<le> n"
+  by (auto intro: power2_le_imp_le power_mono)
+
+lemma power2_nat_le_imp_le:
+  fixes m n :: nat
+  assumes "m\<twosuperior> \<le> n"
+  shows "m \<le> n"
+  using assms by (cases m) (simp_all add: power2_eq_square)
+
+
 
 subsection {* Code generator tweak *}
 
 lemma power_power_power [code]:
   "power = power.power (1::'a::{power}) (op *)"