equal
deleted
inserted
replaced
216 apply (induct n) |
216 apply (induct n) |
217 apply (simp_all split: split_if_asm add: power_Suc) |
217 apply (simp_all split: split_if_asm add: power_Suc) |
218 done |
218 done |
219 |
219 |
220 lemma zero_le_even_power: "even n ==> |
220 lemma zero_le_even_power: "even n ==> |
221 0 <= (x::'a::{linlinordered_ring_strict,monoid_mult}) ^ n" |
221 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n" |
222 apply (simp add: even_nat_equiv_def2) |
222 apply (simp add: even_nat_equiv_def2) |
223 apply (erule exE) |
223 apply (erule exE) |
224 apply (erule ssubst) |
224 apply (erule ssubst) |
225 apply (subst power_add) |
225 apply (subst power_add) |
226 apply (rule zero_le_square) |
226 apply (rule zero_le_square) |