import Mathlib.Tactic

theorem square_mod_four (n : Fin 4) : n.val ^ 2 % 4 = 0 ∨ n.val ^ 2 % 4 = 1 := by decide