Question about Lemma (2.3) in Constructive Analysis, Bishop and Bridges I am in the process of formalizing the constructive notion of a real number and the equivalence on them in the proof assistant Agda, but I am having trouble with the proof of Lemma (2.3) in the following:
In Errett Bishops and Douglas S. Bridges Constructive Analysis from 1985, real numbers are constructively defined as a regular sequence of rational numbers, where regularity of a sequence $x \equiv x_n$ is defined as

$$|x_n - x_m|\leq m^{-1} + n^{-1}$$ For any strictly positive integers
  $n, m$.
And equivalence as
Two real numbers $x \equiv (x_n)$ and $y \equiv (y_n)$ are equal if 
  \begin{equation} | x_n - y_n| \leq 2n^{-1} \end{equation} For all
  strictly positive integers n.
Lemma (2.3) The real numbers $x\equiv(x_n)$ and $y\equiv(y_n)$ are
  equal if and only if for each positive integer $j$ there exists a
  positive integer $N_j$ such that $$|x_n - y_n| \leq j^{-1} \quad (n
> \geq N_j)$$ Proof: If $x=y$ then the lemma holds with $N_j \equiv 2j$
  Assume conversly that for each positive integer j there exists an
  $N_j$ satisfying the relation. Consider a positive integer $n$. If $m$
  and $j$ are any positive integers with $m \geq max(j, N_j)$ then $$
> |x_n - y_n| \leq |x_n - x_m| + |x_m - y_m| + |y_m - y_n| \leq n^{-1}+
> m^{-1} + j^{-1} + m^{-1} + n^{-1} < 2n^{-1} + 3j^{-1}$$ Since this
  holds for any positive integer j, then x and y are equivalent.

The very last part of this proof is what I am having difficulties with. I understand that we can, informally (and perhaps classically?) let $j$ go infinity (although this is hard to express formally in the current framework I'm using) and let $3j^{-1}$ vanish. But how are we to, given an n, constructively choose a j and complete the proof of this lemma?
If it holds for all j, shouldn't it be true in particular for $j = 1$ for example?
Can someone shed some light on this?
 A: Yes, the inequality holds for all $j$. Indeed, for all $j$ (included $j=1$ or whatever) we can choose an auxiliar $m$ satisfaying $m\geq\max(j,N_j)$, for example $\max(j,N_j)$ itself is valid. Independiently of $m$ chosen (given $j$), we have necessarily
$|x_n-y_n|\leq 2 n^{-1} + 3 j^{-j}$ for all $j$. 
This implies that $|x_n-y_n|\leq 2 n^{-1}$ (you can proceed by way of contradiction).
A: Recall that $x$, $y$, and $n$ are rational. For rational numbers, in systems like Bishop's framework for constructive mathematics, we retain much of classical logic. For example, we know in Bishop's system that if $p$ and $q$ are rational then exactly one of $p < q$, $p = q$, or $p > q$ holds. Indeed, if you give me two rational numbers I can determine constructively which of these is the case. 
So, even working constructively, I can work by assuming that $|x_n - y_n| \geq 2n^{-1}$ and obtaining a contradiction. The same technique as the classical proof will work here.  If $|x_n - y_n| > 2n^{-1}$ then we can constructively find a $j$ small enoungh that $|x_n - y_n| > 3j^{-1} + 2n^{-1}$, which is a contrdiction to the inequality established already in the proof. 
One place that a difference will occur with Bishop's system is with real numbers. In Bishop's system, we do not know that for all real numbers $r,s$  we have $r < s$, $r = s$, or $ r > s$, so we cannot prove $r < s$ by showing that $r \geq s$ leads to a contradiction. But we can use that method for natural numbers or rational numbers. 
