Bishop states the constructive or approximate intermediate value theorem on page 40 of Constructive Analysis.
Approx. IVT: Let $f$ be a continuous map on an interval $I$ with $a,b \in I$ and $f(a) < f(b)$. Then for each $y \in [f(a),f(b)]$ and each $\epsilon > 0$, there exists $x \in [min\{a,b\},max\{a,b\}]$ such that $|f(x) - y| \leq \epsilon$.
The first line of the proof says "Since $f$ is continuous we must have $a \neq b$." Recall, in Bishop $a \neq b$ iff either $a < b$ or $b < a$. I'm having some trouble showing this first line rigourously although it seems obvious.
What I can show is that if $f$ is continuous and $f(a) < f(b)$ then $a = b$ leads to contradiction. Thus, $\lnot(a = b)$. But with out decidability of order on the reals I can not take the next step and conclude $a \neq b$. What am I missing?
Let $\omega$ denote a modulus of continuity of $f$ on the interval $I$.
Since $f(a) < f(b)$, we have that $0 < f(b) - f(a)$, so in particular $\frac{|f(b) - f(a)|}{2} = \frac{f(b) - f(a)}{2} > 0$.
So set $\varepsilon = \omega\left(\frac{|f(b) - f(a)|}{2}\right)$. Since $f$ is continuous, we get that if $|b - a| < \varepsilon$ held, then we would have $|f(b) - f(a)| \leq \frac{|f(b) - f(a)|}{2}$, a contradiction. By Lemma 2.18, this means that $|b - a| \geq \varepsilon > 0$, and thus $b \neq a$.