no goals
α : Type ?u.513601
β : Type ?u.513604
ι : Type ?u.513607
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ Tendsto (fun x => ↑⌊x⌋₊ / x) atTop (𝓝 1)
simpa using tendsto_nat_floor_mul_div_atTop (zero_le_one' R)