src/HOL/Power.thy
changeset 33274 b6ff7db522b5
parent 31998 2c7a24f74db9
child 33364 2bd12592c5e8
     1.1 --- a/src/HOL/Power.thy	Wed Oct 28 12:21:38 2009 +0000
     1.2 +++ b/src/HOL/Power.thy	Wed Oct 28 17:44:03 2009 +0100
     1.3 @@ -452,6 +452,12 @@
     1.4    from power_strict_increasing_iff [OF this] less show ?thesis ..
     1.5  qed
     1.6  
     1.7 +lemma power_dvd_imp_le:
     1.8 +  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
     1.9 +  apply (rule power_le_imp_le_exp, assumption)
    1.10 +  apply (erule dvd_imp_le, simp)
    1.11 +  done
    1.12 +
    1.13  
    1.14  subsection {* Code generator tweak *}
    1.15