# HG changeset patch
# User hoelzl
# Date 1334752158 -7200
# Node ID 836b4c4d7c86fe23f35ed0d682ad99b1286e02b7
# Parent  be2ac449488c25dcba304a510b09d5e206fafe52
add powr_inj

diff -r be2ac449488c -r 836b4c4d7c86 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Wed Apr 18 14:29:17 2012 +0200
+++ b/src/HOL/Log.thy	Wed Apr 18 14:29:18 2012 +0200
@@ -285,6 +285,10 @@
   apply (rule powr_less_mono2, auto)
 done
 
+lemma powr_inj:
+  "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
+  unfolding powr_def exp_inj_iff by simp
+
 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
   apply (rule mult_imp_le_div_pos)
   apply (assumption)