removed unnecessary premise from power_le_imp_le_base
authorhuffman
Tue Apr 10 21:50:08 2007 +0200 (2007-04-10)
changeset 226247a6c8ed516ab
parent 22623 5fcee5b319a2
child 22625 a2967023d674
removed unnecessary premise from power_le_imp_le_base
src/HOL/Power.thy
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Power.thy	Tue Apr 10 18:09:58 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Apr 10 21:50:08 2007 +0200
     1.3 @@ -291,8 +291,7 @@
     1.4  
     1.5  lemma power_le_imp_le_base:
     1.6    assumes le: "a ^ Suc n \<le> b ^ Suc n"
     1.7 -      and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"
     1.8 -      and ynonneg: "0 \<le> b"
     1.9 +      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
    1.10    shows "a \<le> b"
    1.11   proof (rule ccontr)
    1.12     assume "~ a \<le> b"
     2.1 --- a/src/HOL/Real/RealPow.thy	Tue Apr 10 18:09:58 2007 +0200
     2.2 +++ b/src/HOL/Real/RealPow.thy	Tue Apr 10 21:50:08 2007 +0200
     2.3 @@ -228,7 +228,7 @@
     2.4  proof -
     2.5    from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
     2.6      by (simp only: numeral_2_eq_2)
     2.7 -  thus "x \<le> y" using xgt0 ygt0
     2.8 +  thus "x \<le> y" using ygt0
     2.9      by (rule power_le_imp_le_base)
    2.10  qed
    2.11