Theorem: IMOSL.IMO2009N2.Even_iff_bodd (IMOSLLean4/IMO2009/N2/N2.lean)

State before:
k : ℕ
⊢ Even k ↔ k.bodd = false
Tactic:
rw [Nat.even_iff, Nat.mod_two_of_bodd, Bool.cond_eq_ite,
  Nat.one_ne_zero.ite_eq_right_iff, Bool.bool_iff_false]
State after:
no goals