(* Authors: Albert Qiaochu Jiang *) theory mathd_algebra_190 imports Complex_Main begin theorem mathd_algebra_190: "((3::real) / 8 + 7 / 8) / (4 / 5) = 25 / 16" by eval end