A classical exercise for beginners in calculus is the following : let $(u_n)$ be a nondecreasing sequence of reals that converges to $0$. Show that $u_n\leq 0$ for all $n$.
There is a variation of course : replace "nondecreasing" by "increasing" and $\leq$ by $<$.
For the purposes of the question, it's important to note that my definition of converging here is $\forall \epsilon >0, \exists N\in \mathbb{N},\forall n\geq N, -\epsilon < u_n < \epsilon$. It's the standard definition but I avoided the use of the absolute value because it cannot be defined without the law of excluded middle.
The classical proof for this either starts with "assume $u_n>0$ (resp. $u_n\geq 0$), then blabla", or if you want to use the LEM later you can fix $n$ and pick $N\geq n$ such that $u_N< |u_n|$ after having dealt with the case where $u_n=0$.
But in those two proofs one really uses the law of excluded middle, perhaps multiple times. Moreover I'm having a hard time finding a proof that doesn't use the LEM. Heuristically, one could say that it's not possible to decide whether $u_n=0$ or not so it's not possible to find $N$ such that $-|u_n| < u_N < |u_n|$ and so to perform the argument.
So my question is natural
Is it possible to prove either of the variants of the above exercise intuitionistically ?
To be clearer on what I mean (since the reals have different models intuitionistically), let me say that any specific intuitionistic model of the reals you like will be fine.
Taking $\epsilon=1/2$, we have that for all sufficiently large $n$, $u_n<1/2$. Therefore, because the $u$’s are non-increasing, for all $n$, $u_n<1/2$. Similarly for all positive integer $n$ and $k$, $u_n < 1/k$. Therefore, by the definition of $\le$ (as in the HoTT book or Bishop & Bridges or any other source for basic constructive definitions), for all $n$, $u_n\le 0$.
If the $u$’s are increasing, then $u_n < u_{n+1} \le 0$, so $u_n < 0$.