import Mathlib.Tactic

theorem square_minus_n_even (n : Fin 100) : 2 ∣ (n.val * n.val - n.val) := by
  decide