isabelle/valid/mathd_numbertheory_84.thy

(*
  Authors: Albert Qiaochu Jiang
*)

theory mathd_numbertheory_84 imports
Complex_Main

begin

theorem mathd_numbertheory_84:
  "floor ((9::real) / 160 * 100) = (5::int)"
  by eval

end