no goals
F : Type ?u.227030
α : Type u_1
β : Type ?u.227036
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ : α
z : ℤ
a : α
ha : a ∈ Ioc (↑z - 1) ↑z
⊢ ↑⌈a⌉ = ↑z
exact_mod_cast ceil_eq_on_Ioc z a ha