src/HOL/Power.thy
changeset 24376 e403ab5c9415
parent 24286 7619080e49f0
child 24996 ebd5f4cc7118
     1.1 --- a/src/HOL/Power.thy	Tue Aug 21 02:15:13 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Aug 21 02:30:14 2007 +0200
     1.3 @@ -77,6 +77,10 @@
     1.4    finally show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma one_less_power:
     1.8 +  "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n"
     1.9 +by (cases n, simp_all add: power_gt1_lemma power_Suc)
    1.10 +
    1.11  lemma power_gt1:
    1.12       "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)"
    1.13  by (simp add: power_gt1_lemma power_Suc)