src/HOL/Divides.thy
 changeset 31009 41fd307cab30 parent 30934 ed5377c2b0a3 child 31661 1e252b8b2334
```     1.1 --- a/src/HOL/Divides.thy	Mon Apr 27 19:44:30 2009 -0700
1.2 +++ b/src/HOL/Divides.thy	Tue Apr 28 13:34:45 2009 +0200
1.3 @@ -333,8 +333,9 @@
1.4
1.5  end
1.6
1.7 -lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
1.8 -    (x div y)^n = x^n div y^n"
1.9 +lemma div_power:
1.10 +  "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \<Longrightarrow>
1.11 +    (x div y) ^ n = x ^ n div y ^ n"
1.12  apply (induct n)
1.13   apply simp
1.15 @@ -936,10 +937,8 @@
1.16  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
1.17    by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
1.18
1.19 -lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
1.20 -  by (induct n) auto
1.21 -
1.22 -lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
1.23 +lemma power_dvd_imp_le:
1.24 +  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
1.25    apply (rule power_le_imp_le_exp, assumption)
1.26    apply (erule dvd_imp_le, simp)
1.27    done
```