equal
deleted
inserted
replaced
356 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
356 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
357 by presburger |
357 by presburger |
358 |
358 |
359 text {* Simplify, when the exponent is a numeral *} |
359 text {* Simplify, when the exponent is a numeral *} |
360 |
360 |
361 lemma power_0_left_numeral [simp]: |
|
362 "0 ^ numeral w = (0::'a::{power,semiring_0})" |
|
363 by (simp add: power_0_left) |
|
364 |
|
365 lemmas zero_le_power_eq_numeral [simp] = |
361 lemmas zero_le_power_eq_numeral [simp] = |
366 zero_le_power_eq [of _ "numeral w"] for w |
362 zero_le_power_eq [of _ "numeral w"] for w |
367 |
363 |
368 lemmas zero_less_power_eq_numeral [simp] = |
364 lemmas zero_less_power_eq_numeral [simp] = |
369 zero_less_power_eq [of _ "numeral w"] for w |
365 zero_less_power_eq [of _ "numeral w"] for w |