Does my attempt look fine or contain logical flaws/gaps? Any suggestion is greatly appreciated. Thank you for your help!
Let $\mathcal{C}$ be the set of Cauchy sequences of rationals. We define an equivalence relation $\sim$ on $\mathcal{C}$ by $$(a_n) \sim (b_n) \iff \forall \epsilon >0, \exists N, \forall n>N: |a_n - b_n| < \epsilon$$
Let $\mathcal{C} / {\sim}$ be the set of all equivalence classes of Cauchy sequences of rationals. We define a relation $\preccurlyeq$ on $\mathcal{C} / {\sim}$ by $$[(a_n)] \preccurlyeq [(b_n)] \iff \forall \epsilon >0, \exists N, \forall n>N: a_n - b_n < \epsilon$$
I have shown that $\preccurlyeq$ is a complete linear ordering here.
I have shown that $[(a_n)] \prec [(b_n)] \iff \exists \epsilon >0, \exists N, \forall n>N: \epsilon \le b_n -a_n$ here.
Theorem: $\Bbb Q$ is dense in $\Bbb R$.
My attempt:
$[(a_n)] \prec [(b_n)] \implies \exists \epsilon' >0, \exists N', \forall n>N': \epsilon \le b_n -a_n$.
$(a_n),(b_n)$ are Cauchy sequences $\implies$ $\exists N'', \forall m,n > N'': |a_m - a_n| < \dfrac{\epsilon'}{4} \wedge |b_m - b_n| < \dfrac{\epsilon'}{4}$.
Let $N_0 = \max \{N'+1,N''+1\}$. It follows that $\epsilon \le b_{N_0} -a_{N_0}$ and $\forall n > N_0: |a_n - a_{N_0}| < \dfrac{\epsilon'}{4} \wedge |b_n - b_{N_0}| < \dfrac{\epsilon'}{4}$.
Let $(x_n)$ be the sequence whose all elements are equal to $\dfrac{a_{N_0} + b_{N_0}}{2}$. It follows directly that $[(x_n)]$ is rational.
Next we prove $[(a_n)] \prec [(x_n)] \prec [(b_n)]$.
$n > N_0 \implies |a_n - a_{N_0}| < \dfrac{\epsilon'}{4} \implies a_n < a_{N_0} + \dfrac{\epsilon'}{4} \implies$ $\dfrac{a_{N_0} + b_{N_0}}{2} - a_n > \dfrac{b_{N_0}-a_{N_0}}{2}-\dfrac{\epsilon'}{4} \ge \dfrac{\epsilon}{2}-\dfrac{\epsilon'}{4} = \dfrac{\epsilon'}{4} \implies$ $\exists \dfrac{\epsilon'}{4} >0, \exists N_0, \forall n>N_0: \dfrac{\epsilon'}{4} \le \dfrac{a_{N_0} + b_{N_0}}{2} -a_n \implies [(a_n)] \prec [(x_n)]$.
$n > N_0 \implies |b_n - b_{N_0}| < \dfrac{\epsilon'}{4} \implies b_{N_0} - \dfrac{\epsilon'}{4} < b_n \implies$ $b_n - \dfrac{a_{N_0} + b_{N_0}}{2} > \dfrac{b_{N_0}-a_{N_0}}{2}-\dfrac{\epsilon'}{4} \ge \dfrac{\epsilon}{2}-\dfrac{\epsilon'}{4} = \dfrac{\epsilon'}{4} \implies$ $\exists \dfrac{\epsilon'}{4} >0, \exists N_0, \forall n>N_0: \dfrac{\epsilon'}{4} \le b_n - \dfrac{a_{N_0} + b_{N_0}}{2} \implies [(x_n)] \prec [(b_n)]$.