remove redundant lemma realpow_increasing

--- a/src/HOL/RealPow.thy	Tue Feb 23 14:38:06 2010 -0800
+++ b/src/HOL/RealPow.thy	Tue Feb 23 14:44:24 2010 -0800
@@ -42,11 +42,6 @@
 apply auto
 done
 
-(* used by AFP Integration theory *)
-lemma realpow_increasing:
-     "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
-  by (rule power_le_imp_le_base)
-
 
 subsection{* Squares of Reals *}