1.1 --- a/src/HOL/Power.thy	Mon May 07 23:07:04 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue May 08 00:50:55 2007 +0200
     1.3 @@ -302,6 +302,18 @@
     1.4        by (simp add: linorder_not_less [symmetric])
     1.5   qed
     1.6  
     1.7 +lemma power_less_imp_less_base:
     1.8 +  fixes a b :: "'a::{ordered_semidom,recpower}"
     1.9 +  assumes less: "a ^ n < b ^ n"
    1.10 +  assumes nonneg: "0 \<le> b"
    1.11 +  shows "a < b"
    1.12 +proof (rule contrapos_pp [OF less])
    1.13 +  assume "~ a < b"
    1.14 +  hence "b \<le> a" by (simp only: linorder_not_less)
    1.15 +  hence "b ^ n \<le> a ^ n" using nonneg by (rule power_mono)
    1.16 +  thus "~ a ^ n < b ^ n" by (simp only: linorder_not_less)
    1.17 +qed
    1.18 +
    1.19  lemma power_inject_base:
    1.20       "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
    1.21        ==> a = (b::'a::{ordered_semidom,recpower})"