equal
deleted
inserted
replaced
200 show ?case by (force simp add: prems power_Suc zero_less_mult_iff) |
200 show ?case by (force simp add: prems power_Suc zero_less_mult_iff) |
201 qed |
201 qed |
202 |
202 |
203 lemma zero_le_power_abs [simp]: |
203 lemma zero_le_power_abs [simp]: |
204 "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n" |
204 "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n" |
205 apply (induct "n") |
205 by (rule zero_le_power [OF abs_ge_zero]) |
206 apply (auto simp add: zero_le_one zero_le_power) |
|
207 done |
|
208 |
206 |
209 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,recpower}) ^ n" |
207 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,recpower}) ^ n" |
210 proof - |
208 proof - |
211 have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric]) |
209 have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric]) |
212 thus ?thesis by (simp only: power_mult_distrib) |
210 thus ?thesis by (simp only: power_mult_distrib) |