removed unnecessary premise from power_le_imp_le_base

--- a/src/HOL/Power.thy	Tue Apr 10 18:09:58 2007 +0200
+++ b/src/HOL/Power.thy	Tue Apr 10 21:50:08 2007 +0200
@@ -291,8 +291,7 @@
 
 lemma power_le_imp_le_base:
   assumes le: "a ^ Suc n \<le> b ^ Suc n"
-      and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"
-      and ynonneg: "0 \<le> b"
+      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
   shows "a \<le> b"
  proof (rule ccontr)
    assume "~ a \<le> b"

--- a/src/HOL/Real/RealPow.thy	Tue Apr 10 18:09:58 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Tue Apr 10 21:50:08 2007 +0200
@@ -228,7 +228,7 @@
 proof -
   from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
     by (simp only: numeral_2_eq_2)
-  thus "x \<le> y" using xgt0 ygt0
+  thus "x \<le> y" using ygt0
     by (rule power_le_imp_le_base)
 qed