I aim to prove some of the order properties of Bishop's Real Numbers (given on page 22 of Constructive Analysis by Bishop and Bridges.) Bishop defines a real number to be a regular sequence of rational numbers, that is, a sequence $(x_n)$ of rational numbers such that $$ |x_m - x_n| \leq m^{-1} + n^{-1}. $$ A real number is positive , or $x \in \mathbb{R}^+$, if $$ x_n > n^{-1} $$ for some $n \in \mathbb{Z}^+$. A real number is nonnegative, or $x \in \mathbb{R}^{0+}$, if $$ x_n \geq -n^{-1} $$ for all $n \in \mathbb{Z}^+$. Bishop goes on to proves a useful criteria, specifically, $x \in \mathbb{R}^+$ iff there exists a $N \in Z^+$ such that $$ x_m \geq N^{-1} $$ for $m \geq N$. Additionally, $x \in \mathbb{R}^{0+}$ iff for every $n \in \mathbb{Z}^+$ there exists $N_n \in \mathbb{Z}^+$ such that $$ x_m \geq -n^{-1} $$ for $m \geq N_n$. The order properties I wish to prove are stated in Proposition 2.9. Specifically, the statement if $x,y \in \mathbb{R}^{0+}$ then $xy \in \mathbb{R}^{0+}$. I’m missing something mechanically about this proof and am seeking insight.
It is surely also relevant to provide the definition of multiplication. Given real numbers $x \equiv (x_n)$ and $y \equiv (y_n)$ we define $xy = (x_{2kn}y_{2kn})$ where $k = max\{K_x,K_y\}$ and $K_x$ is the canonical upper bound of $x$ (i.e. the least integer greater than $|x_1| + 2$.) One can quite easily show that $xy$ is in fact a real number.
Per the construction of $k$ and $xy$ we know that $$x_{2kn}, y_{2kn} \in [-(2kn)^{-1}, k]$$ and therefore $$(xy)_n = x_{2kn}y_{2kn} \geq -(2n)^{-1} > -n^{-1}.$$