[proofplan]
We prove existence by applying the Euclidean algorithm to a reduced fraction $x = m/q$ and reading the successive quotients as the partial quotients of the continued fraction. Termination follows from the strict decrease of the positive remainders. For uniqueness, we show that the first partial quotient is the integer part of the rational number, and then subtracting that integer part and inverting recovers the tail. Iterating this tail-recovery procedure forces all partial quotients to agree; the final-term condition removes the only ambiguity, namely replacing a final entry $a_n$ by $a_n - 1, 1$.
[/proofplan]
[step:Construct the continued fraction from the Euclidean algorithm]
Choose $m,q \in \mathbb{N}$ such that $x = m/q$ and $\gcd(m,q) = 1$. Here $\gcd(m,q)$ denotes the greatest common divisor of the integers $m$ and $q$. Apply the [division algorithm](/theorems/725) recursively as follows. Define integers $r_{-1} := m$ and $r_0 := q$. For each index $k \geq 0$ for which $r_k > 0$, write
\begin{align*}
r_{k-1} = a_k r_k + r_{k+1},
\qquad
0 \leq r_{k+1} < r_k,
\end{align*}
with $a_k \in \mathbb{Z}_{\geq 0}$ when $k = 0$ and $a_k \in \mathbb{N}$ when $k \geq 1$.
The strict inequality $0 \leq r_{k+1} < r_k$ shows that the positive remainders strictly decrease, so the recursion terminates. Since $\gcd(m,q)=1$, the last nonzero remainder is $1$. Hence there is an index $n \geq 0$ such that
\begin{align*}
r_{n-1} = a_n r_n,
\qquad
r_n = 1
\end{align*}
if $n \geq 1$, or $r_1=0$ if $n=0$.
For each $k$ with $0 \leq k \leq n$ and $r_k > 0$, define the rational number
\begin{align*}
x_k := \frac{r_{k-1}}{r_k}.
\end{align*}
Then the division identity gives
\begin{align*}
x_k
= a_k + \frac{r_{k+1}}{r_k}.
\end{align*}
If $k<n$, then $r_{k+1}>0$, so
\begin{align*}
x_k
= a_k + \frac{1}{r_k/r_{k+1}}
= a_k + \frac{1}{x_{k+1}}.
\end{align*}
At the final index, $x_n = a_n$. Substituting these identities backward from $k=n$ to $k=0$ yields
\begin{align*}
x = x_0 = [a_0; a_1,\dots,a_n].
\end{align*}
Thus a finite simple continued fraction expansion exists.
[/step]
[step:Verify that the Euclidean expansion satisfies the final-term convention]
If the construction terminates at $n=0$, then $x = a_0$ and there is no final positive tail coefficient to check. Suppose $n \geq 1$. Since the last nonzero remainder is $r_n=1$, the preceding remainder satisfies $r_{n-1} \in \mathbb{N}$ and
\begin{align*}
r_{n-1} = a_n r_n = a_n.
\end{align*}
If $a_n=1$, then $r_{n-1}=1=r_n$, contradicting the strict decrease $r_n<r_{n-1}$ that holds at the previous Euclidean step. Therefore $a_n>1$.
[/step]
[step:Recover the first partial quotient from the value]
Let
\begin{align*}
y = [b_0;b_1,\dots,b_s]
\end{align*}
be any finite simple continued fraction with $b_0 \in \mathbb{Z}_{\geq 0}$ and $b_1,\dots,b_s \in \mathbb{N}$. If $s=0$, then $y=b_0$. If $s\geq 1$, define
\begin{align*}
t := [b_1;b_2,\dots,b_s].
\end{align*}
Since $b_1 \in \mathbb{N}$ and every later partial quotient is positive, we have $t>1$ when $s\geq 2$ and $t=b_1\geq 1$ when $s=1$. Hence $t \geq 1$, and
\begin{align*}
y = b_0 + \frac{1}{t},
\qquad
0 < \frac{1}{t} \leq 1.
\end{align*}
If $s\geq 1$ and the normalized final-term condition holds, then either $s=1$ and $b_1>1$, or $s\geq 2$ and $t>b_1\geq 1$. In both cases $t>1$, so
\begin{align*}
0 < \frac{1}{t} < 1.
\end{align*}
Let $\lfloor y \rfloor$ denote the value at $y$ of the floor function $\lfloor \cdot \rfloor: \mathbb{R} \to \mathbb{Z}$, namely the greatest integer less than or equal to its argument. Therefore, for a normalized non-integer expansion,
\begin{align*}
b_0 = \lfloor y \rfloor.
\end{align*}
[guided]
The first coefficient must be recoverable from the value of the continued fraction alone. To see this, take an arbitrary finite simple continued fraction
\begin{align*}
y = [b_0;b_1,\dots,b_s],
\end{align*}
where $b_0 \in \mathbb{Z}_{\geq 0}$ and $b_1,\dots,b_s \in \mathbb{N}$.
If $s=0$, then the continued fraction is just the integer $y=b_0$. Now suppose $s\geq 1$. Define the tail rational number
\begin{align*}
t := [b_1;b_2,\dots,b_s].
\end{align*}
Because every tail coefficient is a positive integer, $t\geq 1$. Therefore
\begin{align*}
y = b_0 + \frac{1}{t},
\qquad
0 < \frac{1}{t} \leq 1.
\end{align*}
The endpoint case $\frac{1}{t}=1$ is exactly where the familiar ambiguity comes from: it occurs when $t=1$, which means the tail is just $[1]$. The normalization condition excludes this as the final tail when there is a nonzero tail, because the final coefficient must be greater than $1$. More precisely, if $s=1$, then normalization gives $b_1>1$, so $t=b_1>1$. If $s\geq 2$, then
\begin{align*}
t = b_1 + \frac{1}{[b_2;\dots,b_s]} > b_1 \geq 1.
\end{align*}
Thus in every normalized non-integer case,
\begin{align*}
0 < \frac{1}{t} < 1.
\end{align*}
Let $\lfloor y \rfloor$ denote the value at $y$ of the floor function $\lfloor \cdot \rfloor: \mathbb{R} \to \mathbb{Z}$, namely the greatest integer less than or equal to its argument. This places $y$ strictly between $b_0$ and $b_0+1$, so the integer part is forced:
\begin{align*}
b_0 = \lfloor y \rfloor.
\end{align*}
[/guided]
[/step]
[step:Recover the tail by subtracting the integer part and inverting]
Let
\begin{align*}
y = [b_0;b_1,\dots,b_s]
\end{align*}
be normalized and suppose $s\geq 1$. Define
\begin{align*}
t := [b_1;b_2,\dots,b_s].
\end{align*}
From the previous step, $b_0=\lfloor y\rfloor$ and
\begin{align*}
y-b_0 = \frac{1}{t}.
\end{align*}
Since $t>0$, inversion gives
\begin{align*}
\frac{1}{y-\lfloor y\rfloor} = t = [b_1;b_2,\dots,b_s].
\end{align*}
Thus the value of a normalized non-integer continued fraction determines its tail.
[/step]
[step:Iterate tail recovery to prove uniqueness]
Suppose two normalized finite simple [continued fractions](/page/Continued%20Fractions) have the same value:
\begin{align*}
[a_0;a_1,\dots,a_n] = [b_0;b_1,\dots,b_s].
\end{align*}
If both have length $0$, then both sides are integers, and equality gives $a_0=b_0$.
Assume at least one has positive length. By the first-coefficient recovery step, both first coefficients equal the integer part of the common value, so
\begin{align*}
a_0=b_0.
\end{align*}
If the common value is an integer, then the normalized representation must have length $0$, because a normalized expansion with positive length has fractional part strictly between $0$ and $1$. Hence both expansions are $[a_0]$.
If the common value is not an integer, subtract $a_0=b_0$ and invert. The tail-recovery step gives
\begin{align*}
[a_1;\dots,a_n] = [b_1;\dots,b_s].
\end{align*}
The tails are again normalized finite simple continued fractions: their final coefficients are the same final coefficients as before, hence exceed $1$ when the tail has positive length.
Repeating the same argument for the tails forces equality of the successive coefficients. Since both expansions are finite, the iteration reaches the last coefficient. If one expansion ended earlier than the other, the common remaining value would be an integer on one side and a normalized non-integer continued fraction on the other, which the previous paragraph rules out. Therefore $n=s$ and
\begin{align*}
a_k=b_k
\end{align*}
for every $k \in \{0,1,\dots,n\}$. This proves uniqueness of the normalized expansion.
[/step]