# HG changeset patch
# User nipkow
# Date 1236357545 -3600
# Node ID 495f51ec6ed48bc1670afc945adecd5b5bed528c
# Parent  0e0cb7ac02813a949826acceeceaf4c66781f99b# Parent  b2441b0c8d387b1a681e95cfe14a4a7ee35f29c8
merged

diff -r 0e0cb7ac0281 -r 495f51ec6ed4 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Mar 06 17:21:17 2009 +0100
+++ b/src/HOL/Power.thy	Fri Mar 06 17:39:05 2009 +0100
@@ -338,6 +338,24 @@
   by (rule dvd_trans [OF le_imp_power_dvd])
 
 
+lemma dvd_power_same:
+  "(x::'a::{comm_semiring_1,recpower}) dvd y \<Longrightarrow> x^n dvd y^n"
+by (induct n) (auto simp add: mult_dvd_mono)
+
+lemma dvd_power_le:
+  "(x::'a::{comm_semiring_1,recpower}) dvd y \<Longrightarrow> m >= n \<Longrightarrow> x^n dvd y^m"
+by(rule power_le_dvd[OF dvd_power_same])
+
+lemma dvd_power [simp]:
+  "n > 0 | (x::'a::{comm_semiring_1,recpower}) = 1 \<Longrightarrow> x dvd x^n"
+apply (erule disjE)
+ apply (subgoal_tac "x ^ n = x^(Suc (n - 1))")
+  apply (erule ssubst)
+  apply (subst power_Suc)
+  apply auto
+done
+
+
 subsection{*Exponentiation for the Natural Numbers*}
 
 instantiation nat :: recpower