src/HOL/Power.thy
changeset 24376 e403ab5c9415
parent 24286 7619080e49f0
child 24996 ebd5f4cc7118
equal deleted inserted replaced
24375:4aa80fadc071 24376:e403ab5c9415
    74   also have "\<dots> \<le> a * a^n" using gt1
    74   also have "\<dots> \<le> a * a^n" using gt1
    75     by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le
    75     by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le
    76         zero_le_one order_refl)
    76         zero_le_one order_refl)
    77   finally show ?thesis by simp
    77   finally show ?thesis by simp
    78 qed
    78 qed
       
    79 
       
    80 lemma one_less_power:
       
    81   "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n"
       
    82 by (cases n, simp_all add: power_gt1_lemma power_Suc)
    79 
    83 
    80 lemma power_gt1:
    84 lemma power_gt1:
    81      "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)"
    85      "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)"
    82 by (simp add: power_gt1_lemma power_Suc)
    86 by (simp add: power_gt1_lemma power_Suc)
    83 
    87