feat(data/int/parity): not_even_iff (#1694)

Author: ChrisHughes24

src/data/int/parity.lean

@@ -26,6 +26,9 @@ have ∀ m, 2 * to_nat m = to_nat (2 * m),
 theorem even_iff {n : int} : even n ↔ n % 2 = 0 :=
 ⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩
 
+lemma not_even_iff {n : ℤ} : ¬ even n ↔ n % 2 = 1 :=
+by rw [even_iff, mod_two_ne_zero]
+
 instance : decidable_pred even :=
 λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm
 

src/data/nat/parity.lean

@@ -20,6 +20,9 @@ def even (n : nat) : Prop := 2 ∣ n
 theorem even_iff {n : nat} : even n ↔ n % 2 = 0 :=
 ⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩
 
+lemma not_even_iff {n : ℕ} : ¬ even n ↔ n % 2 = 1 :=
+by rw [even_iff, mod_two_ne_zero]
+
 instance : decidable_pred even :=
 λ n, decidable_of_decidable_of_iff (by apply_instance) even_iff.symm