src/HOL/Power.thy
changeset 17149 e2b19c92ef51
parent 16796 140f1e0ea846
child 21199 2d83f93c3580
     1.1 --- a/src/HOL/Power.thy	Fri Aug 26 08:42:52 2005 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Aug 26 10:01:06 2005 +0200
     1.3 @@ -351,6 +351,13 @@
     1.4  apply (erule dvd_imp_le, simp)
     1.5  done
     1.6  
     1.7 +lemma power_diff:
     1.8 +  assumes nz: "a ~= 0"
     1.9 +  shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)"
    1.10 +  by (induct m n rule: diff_induct)
    1.11 +    (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz)
    1.12 +
    1.13 +
    1.14  text{*ML bindings for the general exponentiation theorems*}
    1.15  ML
    1.16  {*