Order Properties of Constructive Reals (Bishop)
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}.$$
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}.$$