theory Query_19_02_16
imports Complex_Main
begin

lemma
  fixes Y :: real
  shows "Y = Y"
proof -
  have *: "nat (floor (Y / 2)) * nat (floor (2::real)) = nat (floor ((Y / 2) * 2))"
    sorry

  have "(-1::real) ^ nat (floor ((Y / 2) * 2)) =
      (-1::real) ^ (nat (floor (Y/2)) * nat (floor (2::real)))"
    by (simp only: *)
  also have "... = (((-1)::real)^2) ^ (nat (floor (Y/2)))"
    oops
end