Theorem: Misc.Nat.not_even_iff (LeanSAT/Util/Misc.lean)

State before:
n : Nat
⊢ ¬Even n ↔ n % 2 = 1
Tactic:
rw [even_iff, mod_two_ne_zero]
State after:
no goals