diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Power.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -174,6 +174,24 @@
 
 end
 
+context semiring_char_0 begin
+
+lemma numeral_power_eq_of_nat_cancel_iff [simp]:
+  "numeral x ^ n = of_nat y \<longleftrightarrow> numeral x ^ n = y"
+  using of_nat_eq_iff by fastforce
+
+lemma real_of_nat_eq_numeral_power_cancel_iff [simp]:
+  "of_nat y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
+  using numeral_power_eq_of_nat_cancel_iff [of x n y] by (metis (mono_tags))
+
+lemma of_nat_eq_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w = of_nat x \<longleftrightarrow> b ^ w = x"
+  by (metis of_nat_power of_nat_eq_iff)
+
+lemma of_nat_power_eq_of_nat_cancel_iff[simp]: "of_nat x = (of_nat b) ^ w \<longleftrightarrow> x = b ^ w"
+  by (metis of_nat_eq_of_nat_power_cancel_iff)
+
+end
+
 context comm_semiring_1
 begin
 
@@ -568,6 +586,34 @@
   shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
 using assms power2_eq_imp_eq by blast
 
+lemma of_nat_less_numeral_power_cancel_iff[simp]:
+  "of_nat x < numeral i ^ n \<longleftrightarrow> x < numeral i ^ n"
+  using of_nat_less_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] .
+
+lemma of_nat_le_numeral_power_cancel_iff[simp]:
+  "of_nat x \<le> numeral i ^ n \<longleftrightarrow> x \<le> numeral i ^ n"
+  using of_nat_le_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] .
+
+lemma numeral_power_less_of_nat_cancel_iff[simp]:
+  "numeral i ^ n < of_nat x \<longleftrightarrow> numeral i ^ n < x"
+  using of_nat_less_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] .
+
+lemma numeral_power_le_of_nat_cancel_iff[simp]:
+  "numeral i ^ n \<le> of_nat x \<longleftrightarrow> numeral i ^ n \<le> x"
+  using of_nat_le_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] .
+
+lemma of_nat_le_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w \<le> of_nat x \<longleftrightarrow> b ^ w \<le> x"
+  by (metis of_nat_le_iff of_nat_power)
+
+lemma of_nat_power_le_of_nat_cancel_iff[simp]: "of_nat x \<le> (of_nat b) ^ w \<longleftrightarrow> x \<le> b ^ w"
+  by (metis of_nat_le_iff of_nat_power)
+
+lemma of_nat_less_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w < of_nat x \<longleftrightarrow> b ^ w < x"
+  by (metis of_nat_less_iff of_nat_power)
+
+lemma of_nat_power_less_of_nat_cancel_iff[simp]: "of_nat x < (of_nat b) ^ w \<longleftrightarrow> x < b ^ w"
+  by (metis of_nat_less_iff of_nat_power)
+
 end
 
 context linordered_ring_strict