src/HOL/Power.thy
changeset 55811 aa1acc25126b
parent 55718 34618f031ba9
child 56480 093ea91498e6
     1.1 --- a/src/HOL/Power.thy	Fri Feb 28 22:00:13 2014 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Feb 28 17:54:52 2014 +0100
     1.3 @@ -613,7 +613,7 @@
     1.4  lemma self_le_power:
     1.5    fixes x::"'a::linordered_semidom" 
     1.6    shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
     1.7 -  by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right)
     1.8 +  using power_increasing[of 1 n x] power_one_right[of x] by auto
     1.9  
    1.10  lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
    1.11    unfolding One_nat_def by (cases m) simp_all