isabelle/valid/numbertheory_sqmod4in01d.thy

(*
  Authors: Albert Qiaochu Jiang
*)

theory numbertheory_sqmod4in01d imports
  Complex_Main
begin

theorem numbertheory_sqmod4in01d:
  fixes a :: int
  shows "(a^2 mod 4 = 0) \<or> (a^2 mod 4 = 1)"
  sorry

end