src/HOL/Power.thy
changeset 51263 31e786e0e6a7
parent 49824 c26665a197dc
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Power.thy	Sun Feb 24 20:18:32 2013 +0100
     1.2 +++ b/src/HOL/Power.thy	Sun Feb 24 20:29:13 2013 +0100
     1.3 @@ -721,6 +721,18 @@
     1.4    apply (erule dvd_imp_le, simp)
     1.5    done
     1.6  
     1.7 +lemma power2_nat_le_eq_le:
     1.8 +  fixes m n :: nat
     1.9 +  shows "m\<twosuperior> \<le> n\<twosuperior> \<longleftrightarrow> m \<le> n"
    1.10 +  by (auto intro: power2_le_imp_le power_mono)
    1.11 +
    1.12 +lemma power2_nat_le_imp_le:
    1.13 +  fixes m n :: nat
    1.14 +  assumes "m\<twosuperior> \<le> n"
    1.15 +  shows "m \<le> n"
    1.16 +  using assms by (cases m) (simp_all add: power2_eq_square)
    1.17 +
    1.18 +
    1.19  
    1.20  subsection {* Code generator tweak *}
    1.21