[proofplan]
We prove the complete quotient formula by induction on $n$, strengthening the induction hypothesis with the auxiliary bound $-\sqrt{D}<m_n<\sqrt{D}$. The floor identity is proved by writing the integer remainder of $a_0+m_n$ modulo $d_n$; this avoids the invalid estimate that $x<\alpha_n<x+1/d_n$ alone controls the floor. The induction step then subtracts $a_n$, inverts, rationalises the denominator, and uses congruence modulo $d_n$ to prove divisibility of the next denominator. The auxiliary bound gives positivity of $D-m_{n+1}^2$ without invoking any unproved external facts about the square-root recurrence.
[/proofplan]
[step:Establish the initial quotient formula and divisibility]
Since $D$ is not a square, $\sqrt{D} \notin \mathbb{N}$, and therefore
\begin{align*}
a_0 < \sqrt{D} < a_0 + 1.
\end{align*}
By definition, $m_0 = 0$ and $d_0 = 1$, so
\begin{align*}
\frac{\sqrt{D} + m_0}{d_0}
=
\frac{\sqrt{D} + 0}{1}
=
\sqrt{D}
=
\alpha_0.
\end{align*}
Also $d_0 = 1 > 0$, and $1$ divides $D - m_0^2 = D$. Since $m_0=0$ and $D\in\mathbb{N}$ is nonsquare, we also have the auxiliary bound
\begin{align*}
-\sqrt{D}<m_0<\sqrt{D}.
\end{align*}
Finally,
\begin{align*}
a_0 = \lfloor \sqrt{D} \rfloor = \lfloor \alpha_0 \rfloor.
\end{align*}
Thus all asserted properties hold for $n=0$.
[/step]
[step:Show that the recurrence floor agrees with the complete quotient floor]
Assume that, for some $n \ge 0$,
\begin{align*}
\alpha_n = \frac{\sqrt{D} + m_n}{d_n},
\end{align*}
with $d_n$ a positive integer. Define the integer remainder $r_n$ by
\begin{align*}
r_n := a_0+m_n-d_n a_n.
\end{align*}
Since the recurrence defines
\begin{align*}
a_n = \left\lfloor \frac{a_0 + m_n}{d_n} \right\rfloor,
\end{align*}
the defining property of the floor gives
\begin{align*}
0\le r_n<d_n.
\end{align*}
Using the induction formula for $\alpha_n$ and the definition of $r_n$, we compute
\begin{align*}
\alpha_n-a_n=\frac{\sqrt{D}+m_n}{d_n}-a_n.
\end{align*}
Combining the two terms over the common positive denominator $d_n$ gives
\begin{align*}
\alpha_n-a_n=\frac{\sqrt{D}+m_n-d_n a_n}{d_n}.
\end{align*}
Since $r_n=a_0+m_n-d_n a_n$, this becomes
\begin{align*}
\alpha_n-a_n=\frac{\sqrt{D}-a_0+r_n}{d_n}.
\end{align*}
Because $a_0=\lfloor\sqrt{D}\rfloor$ and $D$ is nonsquare, $0<\sqrt{D}-a_0<1$. Together with $0\le r_n<d_n$, this gives
\begin{align*}
0<\sqrt{D}-a_0+r_n<d_n.
\end{align*}
Dividing by the positive integer $d_n$ yields
\begin{align*}
0<\alpha_n-a_n<1.
\end{align*}
Equivalently,
\begin{align*}
a_n<\alpha_n<a_n+1,
\end{align*}
and therefore
\begin{align*}
a_n=\lfloor\alpha_n\rfloor.
\end{align*}
[guided]
The quantity that controls the floor is not merely the size of the interval between $(a_0+m_n)/d_n$ and $\alpha_n$; it is the fractional part of $(a_0+m_n)/d_n$. We encode that fractional part by defining the integer remainder
\begin{align*}
r_n := a_0+m_n-d_n a_n.
\end{align*}
This is an integer because $a_0$, $m_n$, $d_n$, and $a_n$ are integers. Since
\begin{align*}
a_n=\left\lfloor \frac{a_0+m_n}{d_n}\right\rfloor
\end{align*}
and $d_n>0$, the floor inequality
\begin{align*}
a_n\le \frac{a_0+m_n}{d_n}<a_n+1
\end{align*}
is equivalent, after multiplying by $d_n$, to
\begin{align*}
0\le a_0+m_n-d_n a_n<d_n.
\end{align*}
Thus
\begin{align*}
0\le r_n<d_n.
\end{align*}
Now use the induction hypothesis for the complete quotient:
\begin{align*}
\alpha_n=\frac{\sqrt{D}+m_n}{d_n}.
\end{align*}
Subtracting $a_n$ gives
\begin{align*}
\alpha_n-a_n=\frac{\sqrt{D}+m_n}{d_n}-a_n.
\end{align*}
Combining the two terms over the common positive denominator $d_n$ gives
\begin{align*}
\alpha_n-a_n=\frac{\sqrt{D}+m_n-d_n a_n}{d_n}.
\end{align*}
Because $r_n=a_0+m_n-d_n a_n$, equivalently $m_n-d_n a_n=r_n-a_0$, we obtain
\begin{align*}
\alpha_n-a_n=\frac{\sqrt{D}-a_0+r_n}{d_n}.
\end{align*}
The hypothesis that $D$ is nonsquare matters here: it implies $\sqrt{D}$ is not an integer, so from $a_0=\lfloor\sqrt{D}\rfloor$ we get the strict bound
\begin{align*}
0<\sqrt{D}-a_0<1.
\end{align*}
Combining this with $0\le r_n<d_n$ gives
\begin{align*}
0<\sqrt{D}-a_0+r_n<1+(d_n-1)=d_n.
\end{align*}
After division by the positive integer $d_n$, we obtain
\begin{align*}
0<\alpha_n-a_n<1.
\end{align*}
Hence
\begin{align*}
a_n<\alpha_n<a_n+1.
\end{align*}
This proves that $a_n$ is the unique integer immediately below $\alpha_n$, so
\begin{align*}
a_n=\lfloor\alpha_n\rfloor.
\end{align*}
[/guided]
[/step]
[step:Rationalise the next complete quotient]
The previous step gives $a_n<\alpha_n<a_n+1$, so $\alpha_n-a_n>0$. Hence the next complete quotient is well-defined by
\begin{align*}
\alpha_{n+1}=\frac{1}{\alpha_n-a_n}.
\end{align*}
Substituting the induction hypothesis gives
\begin{align*}
\alpha_{n+1}=\frac{1}{\frac{\sqrt D+m_n}{d_n}-a_n}.
\end{align*}
Combining the denominator over $d_n$ gives
\begin{align*}
\alpha_{n+1}=\frac{d_n}{\sqrt D+m_n-d_n a_n}.
\end{align*}
By the recurrence definition $m_{n+1}=d_n a_n-m_n$, the denominator is $\sqrt D-m_{n+1}$, and therefore
\begin{align*}
\alpha_{n+1}=\frac{d_n}{\sqrt D-m_{n+1}}.
\end{align*}
Since $m_{n+1}$ is an integer and $\sqrt{D}$ is irrational because $D$ is nonsquare, $\sqrt{D}-m_{n+1}\neq 0$. Thus multiplying numerator and denominator by $\sqrt{D}+m_{n+1}$ is valid and yields
\begin{align*}
\alpha_{n+1}=\frac{d_n(\sqrt D+m_{n+1})}{D-m_{n+1}^2}.
\end{align*}
Once $d_{n+1}=(D-m_{n+1}^2)/d_n$ is shown to be a positive integer in the next step, this identity becomes
\begin{align*}
\alpha_{n+1}=\frac{\sqrt D+m_{n+1}}{d_{n+1}}.
\end{align*}
[/step]
[step:Propagate divisibility, positivity, and the auxiliary bound to the next denominator]
First prove divisibility independently of the definition of $d_{n+1}$. The induction hypothesis gives $d_n\mid D-m_n^2$, and the recurrence gives
\begin{align*}
m_{n+1}=d_n a_n-m_n.
\end{align*}
Therefore $m_{n+1}\equiv -m_n \pmod{d_n}$, so $m_{n+1}^2\equiv m_n^2 \pmod{d_n}$. It follows that
\begin{align*}
D-m_{n+1}^2\equiv D-m_n^2\equiv 0 \pmod{d_n}.
\end{align*}
Thus $d_n$ divides $D-m_{n+1}^2$, and the recurrence formula
\begin{align*}
d_{n+1}=\frac{D-m_{n+1}^2}{d_n}
\end{align*}
defines an integer.
It remains to prove that this integer is positive. From the previous step, $a_n<\alpha_n<a_n+1$. Substituting
\begin{align*}
\alpha_n=\frac{\sqrt{D}+m_n}{d_n}
\end{align*}
and multiplying by the positive integer $d_n$ gives
\begin{align*}
d_n a_n<\sqrt{D}+m_n<d_n(a_n+1).
\end{align*}
Subtracting $m_n$ from the left inequality gives
\begin{align*}
m_{n+1}=d_n a_n-m_n<\sqrt{D}.
\end{align*}
For the lower bound, the same floor identity gives $a_n=\lfloor\alpha_n\rfloor$. Since $\alpha_n>0$, we have $a_n\ge 0$. The strengthened induction hypothesis gives $m_n<\sqrt{D}$, and hence
\begin{align*}
m_{n+1}=d_n a_n-m_n\ge -m_n> -\sqrt{D}.
\end{align*}
Therefore
\begin{align*}
-\sqrt{D}<m_{n+1}<\sqrt{D}.
\end{align*}
This auxiliary bound implies both factors in
\begin{align*}
D-m_{n+1}^2=(\sqrt D-m_{n+1})(\sqrt D+m_{n+1})
\end{align*}
are positive, so
\begin{align*}
D-m_{n+1}^2>0.
\end{align*}
Since $d_n>0$, the quotient
\begin{align*}
d_{n+1}=\frac{D-m_{n+1}^2}{d_n}
\end{align*}
is a positive integer. Substituting this definition into the rationalised identity from the previous step gives
\begin{align*}
\alpha_{n+1}=\frac{\sqrt D+m_{n+1}}{d_{n+1}}.
\end{align*}
Consequently the strengthened induction hypotheses are valid at index $n+1$.
[/step]
[step:Conclude the strengthened induction]
The initial step proves the desired assertions for $n=0$, including the auxiliary bound $-\sqrt{D}<m_0<\sqrt{D}$. The induction steps show that, whenever the strengthened assertions hold at index $n$, they also hold at index $n+1$. Therefore, for every $n \ge 0$,
\begin{align*}
\alpha_n = \frac{\sqrt{D} + m_n}{d_n},
\end{align*}
with $d_n \in \mathbb{N}$, $d_n > 0$, $d_n$ dividing $D-m_n^2$, and
\begin{align*}
a_n = \lfloor \alpha_n \rfloor.
\end{align*}
Discarding the auxiliary bound, these are exactly the asserted complete quotient properties for the continued fraction expansion of $\sqrt{D}$.
[/step]
