Quotient of polynomials, PID but not Euclidean domain?

While trying to look up examples of PIDs that are not Euclidean domains, I found a statement (without reference) on the Euclidean domain page of Wikipedia that

$$\mathbb{R}[X,Y]/(X^2+Y^2+1)$$

is such a ring. After a good deal of searching, I have not been able to find any other (online) reference to this ring.

Can anyone confirm this result? Is there a reference for it (paper, textbook or website)?

In P. Samuel, Anneaux factoriels, pages 36-37, it's proved that $A=\mathbb R[X,Y]/(X^2+Y^2+1)$ is a UFD.

In the following we denote by $x,y$ the residue classes of $X,Y$ modulo $(X^2+Y^2+1)$. Thus $A=\mathbb R[x,y]$ with $x^2+y^2+1=0$.

Lemma. The prime ideals of $A$ are of the form $(ax+by+c)$ with $(a,b)\neq (0,0)$.

Proof. It's not difficult to see that these elements are prime: if $p=ax+by+c$ with $(a,b)\neq (0,0)$, then $A/pA\simeq\mathbb C$.
On the other hand, let $\mathfrak p$ be a non-zero prime ideal of $A$. Since $\dim A=1$ necessarily $\mathfrak p$ is maximal, so $A/\mathfrak p$ is a field. It's enough to show that $\mathfrak p$ contains an element of the form $ax+by+c$ with $(a,b)\neq (0,0)$. Note that $A/\mathfrak p=\mathbb R[\hat x,\hat y]$ and $\hat x,\hat y$ are algebraic over $\mathbb R$. Thus we have an algebraic field extension $\mathbb R\subset A/\mathfrak p$, and therefore $[A/\mathfrak p:\mathbb R]\le2$. In particular, the elements $\hat 1,\hat x,\hat y$ of $A/\mathfrak p$ are linearly dependent over $\mathbb R$.

Let $S\subset A$ be the multiplicative set generated by all prime elements $ax+by+c$ with $(a,b)\neq (0,0)$. The ring of fractions $S^{-1}A$ has no non-zero prime ideals, and therefore $S^{-1}A$ is a field, hence a UFD. Now we can apply Nagata's criterion for factoriality to conclude that $A$ is a UFD.

It's easily seen that $A$ also a PID (use this result.)

Let's prove that $A$ is not Euclidean.

Lemma. Let $A$ be a Euclidean domain. Then there is $p\in A-\{0\}$ prime such that $\pi(A^{\times})=(A/pA)^{\times}$, where $\pi:A\to A/pA$ is the canonical surjection.

Proof. If one considers $p$ a non-zero, non-invertible element with $\delta(p)$ minimal (here $\delta$ is an Euclidean algorithm), then $p$ is prime and for $\hat a\in A/pA$ invertible there is $u\in A$ invertible such that $u-a\in pA$ (write $a=px+u$ with $\delta(u)<\delta(p)$ and notice that $u$ is not $0$ - here one uses that $\hat a$ is invertible -, and necessarily invertible), that is, $\pi(A^{\times})=(A/pA)^{\times}$.

In our case $A^{\times}=\mathbb R^{\times}$. Since $A/pA\simeq\mathbb C$ for any prime $p\in A$, we have $(A/pA)^{\times}\simeq\mathbb C^{\times}$. If we assume that $A$ is Euclidean, then we get a surjective group homomorphism $\mathbb R^{\times}\to\mathbb C^{\times}$ which is also injective (see @zcn's comment below), a contradiction.

Here are some more details for those who, like me, are not so familiar with this material.

$1$) Take a non-zero prime ideal. We wish to show that it is maximal. It contains a prime element (since we are in a UFD, choose an element with a shortest factorisation). Take this to be $ax+by+c$. We will show that the ideal is maximal by showing that the quotient ring by this ideal is a field.

Using the relation $ax+by+c=0$ we can express any element as a polynomial in $x$ with coefficients in $\mathbb{R}$. With the quadratic relation we can make this a linear expression. In searching for an inverse we get two equations in two unknowns, and the determinant of the corresponding matrix is non-zero.

$2$) Non-zero, non-invertible elements exist because otherwise we would be in a field and wouldn't be trying to prove the lemma in the first place.

$3$) Suppose $p$ is not prime. Then there exist $a$ and $b$ such that $p\mid ab$ but $p\nmid a$ and $p\nmid b$. Write $a=q_a p+r_a$ with $\delta(r_a)<\delta(p)$. Then $r_a$ is invertible, with inverse $s_a$. Similarly, we have $q_b$, $r_b$, $s_b$.

Then $ab=q_a (q_b p+r_b)p +q_b r_a p +r_b r_a$, so $p\mid r_a r_b$. Then $p\mid r_a s_a r_b s_b =1$, a contradiction.

$4$) $A^{\times}=\mathbb{R}^{\times}$ follows because every element of $A$ can be uniquely represented as $p(y)+x q(y)$ for polynomials $p$ and $q$.

$5$) From $1$) we know that each element of $A/pA$ can be expressed as a linear expression in $x$, and we have one relation $x^2(a^2+b^2)+2acx+c^2+1=0$. The roots of this are non-real, so by sending $x$ to one of them we can define an isomorphism to $\mathbb{C}$.

$6$) The projection homomorphism is injective because having an invertible element in $pA$ would show that $p$ is also invertible.

$7$) $\mathbb{R}^{\times}$ and $\mathbb{C}^{\times}$ are not isomorphic because $\mathbb{C}^{\times}$ has order $4$ elements whereas $\mathbb{R}^{\times}$ does not (see linked question).