Every natural is even or odd

import Mathlib

theorem nat_even_or_odd (n : Nat) : (∃ k, n = 2 * k) ∨ (∃ k, n = 2 * k + 1) :=by
  rcases Nat.even_or_odd n with h | h
  · left
    rcases h with ⟨k, rfl⟩
    use k
    ring
  · right
    rcases h with ⟨k, rfl⟩
    use k