∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (x : α), Filter.Tendsto Int.ceil (nhdsWithin x (Set.Iic x)) (pure ⌈x⌉)