equal
deleted
inserted
replaced
192 proof (induct "n") |
192 proof (induct "n") |
193 case 0 |
193 case 0 |
194 show ?case by (simp add: zero_less_one) |
194 show ?case by (simp add: zero_less_one) |
195 next |
195 next |
196 case (Suc n) |
196 case (Suc n) |
197 show ?case by (force simp add: prems power_Suc zero_less_mult_iff) |
197 show ?case by (auto simp add: prems power_Suc zero_less_mult_iff |
|
198 abs_zero) |
198 qed |
199 qed |
199 |
200 |
200 lemma zero_le_power_abs [simp]: |
201 lemma zero_le_power_abs [simp]: |
201 "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n" |
202 "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n" |
202 by (rule zero_le_power [OF abs_ge_zero]) |
203 by (rule zero_le_power [OF abs_ge_zero]) |