theorem Nat.odd_succ {n : ℕ} : Odd n.succ ↔ ¬Odd n

theorem Nat.not_even {n : ℕ} : ¬Even n ↔ Odd n

theorem Nat.not_odd {n : ℕ} : ¬Odd n ↔ Even n