feat(data/int/parity, data/nat/parity): add some lemmas (#7624)

Author: Ruben-VandeVelde

src/data/int/parity.lean

@@ -27,12 +27,6 @@ local attribute [simp] -- euclidean_domain.mod_eq_zero uses (2 ∣ n) as normal
 theorem mod_two_ne_zero : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
-@[simp] theorem even_coe_nat (n : ℕ) : even (n : ℤ) ↔ even n :=
-have ∀ m, 2 * to_nat m = to_nat (2 * m),
- from λ m, by cases m; refl,
-⟨λ ⟨m, hm⟩, ⟨to_nat m, by rw [this, ←to_nat_coe_nat n, hm]⟩,
- λ ⟨m, hm⟩, ⟨m, by simp [hm]⟩⟩
-
 theorem even_iff : even n ↔ n % 2 = 0 :=
 ⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩
 
@@ -158,9 +152,12 @@ theorem odd.of_mul_left (h : odd (m * n)) : odd m :=
 theorem odd.of_mul_right (h : odd (m * n)) : odd n :=
 (odd_mul.mp h).2
 
-@[parity_simps] theorem even_pow {n : ℕ} : even (m^n) ↔ even m ∧ n ≠ 0 :=
+@[parity_simps] theorem even_pow {n : ℕ} : even (m ^ n) ↔ even m ∧ n ≠ 0 :=
 by { induction n with n ih; simp [*, even_mul, pow_succ], tauto }
 
+theorem even_pow' {n : ℕ} (h : n ≠ 0) : even (m ^ n) ↔ even m :=
+even_pow.trans $ and_iff_left h
+
 @[parity_simps] theorem odd_add : odd (m + n) ↔ (odd m ↔ even n) :=
 by rw [odd_iff_not_even, even_add, not_iff, odd_iff_not_even]
 
@@ -195,6 +192,18 @@ begin
   simp with parity_simps
 end
 
+@[simp, norm_cast] theorem even_coe_nat (n : ℕ) : even (n : ℤ) ↔ even n :=
+by rw_mod_cast [even_iff, nat.even_iff]
+
+@[simp, norm_cast] theorem odd_coe_nat (n : ℕ) : odd (n : ℤ) ↔ odd n :=
+by rw [odd_iff_not_even, nat.odd_iff_not_even, even_coe_nat]
+
+@[simp] theorem nat_abs_even : even n.nat_abs ↔ even n :=
+coe_nat_dvd_left.symm
+
+@[simp] theorem nat_abs_odd : odd n.nat_abs ↔ odd n :=
+by rw [odd_iff_not_even, nat.odd_iff_not_even, nat_abs_even]
+
 -- Here are examples of how `parity_simps` can be used with `int`.
 
 example (m n : ℤ) (h : even m) : ¬ even (n + 3) ↔ even (m^2 + m + n) :=

src/data/nat/parity.lean

@@ -164,9 +164,12 @@ theorem odd.of_mul_right (h : odd (m * n)) : odd n :=
 
 /-- If `m` and `n` are natural numbers, then the natural number `m^n` is even
 if and only if `m` is even and `n` is positive. -/
-@[parity_simps] theorem even_pow : even (m^n) ↔ even m ∧ n ≠ 0 :=
+@[parity_simps] theorem even_pow : even (m ^ n) ↔ even m ∧ n ≠ 0 :=
 by { induction n with n ih; simp [*, pow_succ', even_mul], tauto }
 
+theorem even_pow' (h : n ≠ 0) : even (m ^ n) ↔ even m :=
+even_pow.trans $ and_iff_left h
+
 theorem even_div : even (m / n) ↔ m % (2 * n) / n = 0 :=
 by rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, nat.div_mod_eq_mod_mul_div, mul_comm]