diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Power.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -501,6 +501,14 @@
     done
 qed
 
+lemma power_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m \<le> b ^ n \<longleftrightarrow> n \<le> m"
+  using power_strict_decreasing [of m n b]
+  by (auto intro: power_decreasing ccontr)
+
+lemma power_strict_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m < b ^ n \<longleftrightarrow> n < m"
+  using power_decreasing_iff [of b m n] unfolding le_less
+  by (auto dest: power_strict_decreasing le_neq_implies_less)
+
 lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   using power_strict_decreasing [of 0 "Suc n" a] by simp