Theorem: Bézout's Identity/Euclidean Domain

Let $\struct {D, +, \times}$ be a Euclidean domain whose zero is $0$ and whose unity is $1$.
Let $\nu: D \setminus \set 0 \to \N$ be the Euclidean valuation on $D$.
Let $a, b \in D$ such that $a$ and $b$ are not both equal to $0$.
Let $\gcd \set {a, b}$ be the greatest common divisor of $a$ and $b$.
Then:
:$\exists x, y \in D: a \times x + b \times y = \gcd \set {a, b}$
such that $\gcd \set {a, b}$ is the element of $D$ such that:
:$\forall c = a \times x + b \times y \in D: \map \nu {\gcd \set {a, b} } \le \map \nu c$

Proof:
{{Proofread}}
We are given that $a, b \in D$ such that $a$ and $b$ are not both equal to $0$.
{{WLOG}}, suppose specifically that $b \ne 0$.
Let $S \subseteq D$ be the set defined as:
:$S = \set {x \in D_{\ne 0}: x = m \times a + n \times b: m, n \in D}$
where $D_{\ne 0}$ denotes $D \setminus 0$.
Setting $m = 0$ and $n = 1$, for example, it is noted that $b \in S$.
Therefore $S \ne \O$.
By definition, $\nu$ has the properties:
:$(1): \quad \forall a, b \in D, b \ne 0: \exists q, r \in D$ such that $\map \nu r < \map \nu b$, or $r = 0$, such that:
::::$a = q \times b + r$
:$(2): \quad \forall a, b \in D, b \ne 0$:
::::$\map \nu a \le \map \nu {a \times b}$
Let $\nu \sqbrk S$ denote the image of $S$ under $\nu$.
We have that:
:$\nu \sqbrk S \subseteq \N$
Hence by the Well-Ordering Principle $\nu \sqbrk S$ has a smallest element.
Let $d \in S$ be such that $\map \nu d$ is that smallest element of $\nu \sqbrk S$.
By definition of $S$, we have that:
:$d = u \times a + v \times b$
for some $u, v \in D$.
Let $x \in S$.
By $(2)$ above:
:$x = q \times d + r$
such that either:
:$\map \nu r < \map \nu d$
or:
:$r = 0$
{{AimForCont}} $r \ne 0$.
Then:
{{begin-eqn}}
{{eqn | q = \exists m, n \in D
      | l = x
      | r = m \times a + n \times b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r
      | r = x - q \times d
      | c = 
}}
{{eqn | r = \paren {m \times a + n \times b} - q \paren {u \times a + v \times b}
      | c = 
}}
{{eqn | r = \paren {m - q \times u} a + \paren {n - q \times v} b
      | c = 
}}
{{eqn | ll= \leadsto
      | o =
      | r = \paren {r \in S} \land \paren {\map \nu r < \map \nu d}
      | c = 
}}
{{end-eqn}}
which contradicts the choice of $d$ as the element of $S$ such that $\map \nu d$ is the smallest element of $\nu \sqbrk S$.
Therefore:
:$\forall x \in S: x = q \times d$
for some $q \in D$.
That is:
:$\forall x \in S: d \divides x$
where $\divides$ denotes divisibility.
In particular:
:$d \divides a = 1 \times a + 0 \times b$
:$d \divides b = 0 \times a + 1 \times b$
Thus:
:$d \divides a \land d \divides b \implies \map \nu 1 \le \map \nu d \le \map \nu {\gcd \set {a, b} }$
However, note that as $\gcd \set {a, b}$ also divides $a$ and $b$ (by definition), we have:
{{begin-eqn}}
{{eqn | l = \gcd \set {a, b}
      | o = \divides
      | r = \paren {u \times a + v \times b} = d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \gcd \set {a, b}
      | o = \divides
      | r = d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \nu {\gcd \set {a, b} }
      | o = \le
      | r = \map \nu d
      | c = 
}}
{{end-eqn}}
Since $d$ is the element of $S$ such that $\map \nu d$ is the smallest element of $\nu \sqbrk S$:
:$\gcd \set {a, b} = d = u \times a + v \times b$
{{qed}}