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

leanprover-community · Nov 17, 2019 · 1034357 · 1034357
1 parent e863c08
commit 1034357
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/src/data/int/parity.lean b/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
 

diff --git a/src/data/nat/parity.lean b/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