no goals
F : Type ?u.311143
α : Type u_1
β : Type ?u.311149
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ⌈a⌉
rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg ha)]