I'm trying to show that $\Bbb Z[\sqrt d]$ is an ordered ring, where $d$ is a positive non-square integer. This is obviously true given that $\Bbb Z[\sqrt d]\subseteq\Bbb R$, but here the catch is that I am working in a weak axiomatic framework, barely stronger than $\sf PA$, so I am trying to work with a barebones encoding of $\Bbb Z[\sqrt d]$ and prove everything relative to the encoding.
Define $\Bbb Z[\sqrt d]:=\Bbb Z\times\Bbb Z$, and let $(x,y)+(x',y')=(x+x',y+y')$ and $(x,y)(x',y')=(xx'+dyy',xy'+yx')$. Given these definitions, it is possible to show that $\Bbb Z[\sqrt d]$ is a ring, simply by unfolding all the definitions and using ring axioms of $\Bbb Z$.
$\Bbb Z$ itself is defined as the disjoint union of two copies of $\Bbb N$, so that every integer $x$ is of the form $n$ or $-(n+1)$ where $n\in\Bbb N$. Given this, we can define $P(x,y)$ (which asserts that $(x,y)$ is nonnegative) by case analysis (where $m,n$ are variables in $\Bbb N$): \begin{align} P(m,n)&\equiv\top\\ P(m,-(n+1))&\equiv m^2\ge d(n+1)^2\\ P(-(m+1),n)&\equiv (m+1)^2\le dn^2\\ P(-(m+1),-(n+1))&\equiv \bot\\ \end{align}
and then say that $(x,y)\le(x',y')$ iff $P(x'-x,y'-y)$.
This definition is correct in the sense that under the interpretation $(x,y)\mapsto x+y\sqrt d$ we have the usual meanings of $+,\cdot,\le$, but the case analysis leads to a lot of cases to check, and I wonder if there isn't a better way. Currently, I'm stuck on showing that $P(a)\wedge P(b)\to P(ab)$, which involves roughly 64 cases (since $x,y,x',y',xx'+dyy',xy'+yx'$ can all be positive or negative), each of which involves some inequality on the natural numbers like:
$$x^2\ge d(y+1)^2,\ \ d (y+1) w+i=xz,\ \ xw+(j+1) = (y+1)z\ \vdash \ i^2\le d(j+1)^2.$$
(This is the case where $a=(x,-(y+1)), b=(z,w), ab=(i,-(j+1))$.) Is there a better way? Although I think it is possible to finish the proof in this manner, I get the strong feeling that I have made this more complicated than it needs to be, especially since the proof over the reals is so simple.