Orderable Topology on Naturals

Stream: general

[Rohan Mitta]

I'm trying to use the squeeze theorem (tendsto_of_tendsto_of_tendsto_of_le_of_le from topological_structures) on a sequence from the naturals to the reals, but I get the error failed to synthesize type class instance for orderable_topology \N

What should I do?

[Rohan Mitta]

Sorry, ignore this, I made a silly mistake