no goals
F : Type ?u.41083
α : Type u_1
β : Type ?u.41089
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ n : ℕ
x : α
hx : x ∈ Ico (↑n) (↑n + 1)
⊢ ↑⌊x⌋₊ = ↑n
exact_mod_cast floor_eq_on_Ico n x hx