I think your definition depends on being able to decide for every real x whether n ∈ [x-1, x), for which you need that n < x. According to the slides that is no

I think your definition depends on being able to decide for every real x whether n ∈ [x-1, x), for which you need that n < x. According to the slides that is not generally possible in constructive mathematics.