# HG changeset patch
# User huffman
# Date 1178578255 -7200
# Node ID 7f000a38560693314f1dea38005fa3b152a249ba
# Parent  2490d4b4671a463ac97a42236552e055800d5853
add lemma power_less_imp_less_base

diff -r 2490d4b4671a -r 7f000a385606 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon May 07 23:07:04 2007 +0200
+++ b/src/HOL/Power.thy	Tue May 08 00:50:55 2007 +0200
@@ -302,6 +302,18 @@
       by (simp add: linorder_not_less [symmetric])
  qed
 
+lemma power_less_imp_less_base:
+  fixes a b :: "'a::{ordered_semidom,recpower}"
+  assumes less: "a ^ n < b ^ n"
+  assumes nonneg: "0 \<le> b"
+  shows "a < b"
+proof (rule contrapos_pp [OF less])
+  assume "~ a < b"
+  hence "b \<le> a" by (simp only: linorder_not_less)
+  hence "b ^ n \<le> a ^ n" using nonneg by (rule power_mono)
+  thus "~ a ^ n < b ^ n" by (simp only: linorder_not_less)
+qed
+
 lemma power_inject_base:
      "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
       ==> a = (b::'a::{ordered_semidom,recpower})"