no goals
F : Type ?u.309882
α : Type u_1
β : Type ?u.309888
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ⌊a⌋
rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)]