equal
deleted
inserted
replaced
346 apply (subst power_abs [THEN sym]) |
346 apply (subst power_abs [THEN sym]) |
347 apply (simp add: zero_le_even_power) |
347 apply (simp add: zero_le_even_power) |
348 done |
348 done |
349 |
349 |
350 lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" |
350 lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" |
351 apply (induct n) |
351 by (induct n, auto) |
352 apply simp |
|
353 apply auto |
|
354 done |
|
355 |
352 |
356 lemma power_minus_even [simp]: "even n ==> |
353 lemma power_minus_even [simp]: "even n ==> |
357 (- x)^n = (x^n::'a::{recpower,comm_ring_1})" |
354 (- x)^n = (x^n::'a::{recpower,comm_ring_1})" |
358 apply (subst power_minus) |
355 apply (subst power_minus) |
359 apply simp |
356 apply simp |