(* 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 \ 2 < sqrt n} = 8" sorry end