isabelle/valid/mathd_algebra_224.thy

(*
  Authors: Wenda Li
*)

theory mathd_algebra_224 
  imports Complex_Main "HOL-Computational_Algebra.Computational_Algebra"
  "HOL-Number_Theory.Number_Theory"
begin

theorem mathd_algebra_224:
  "card { n :: nat. sqrt n < 7 / 2 \<and> 2 < sqrt n} = 8"
  sorry

end