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

State before:
n : Nat
⊢ Xor' (Even n) (Odd n)
Tactic:
simp only [Xor', odd_iff_not_even, Classical.not_not, and_self, Decidable.em (Even n)]
State after:
no goals