import Mathlib

lemma not_odd {n : ℕ} : ¬ Odd n ↔ Even n := by sorry

lemma not_even {n : ℕ} : ¬ Even n ↔ Odd n := by sorry

lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by
  intro ⟨x, hx⟩
  unfold Even at *
  use 2 * x ^ 2
  rw [hx]
  ring
