Square roots proved irrational by denominator descent 
Is this proof correct?

Suppose that $\sqrt{2}=\frac{a}{b}$, where $a,b \in \mathbb{N}$ and $a$ is as small as possible. Then $\sqrt{2}b=a$ which means $2b=\sqrt{2} a$. So we rewrite $\sqrt{2}=\frac{a}{b}\cdot\frac{\sqrt{2}-1}{\sqrt{2}-1}=\frac{\sqrt{2}a-a}{\sqrt{2}b-b}=\frac{2b-a}{a-b}.\,$ Note  $\,2b-a=a(\sqrt{2}-1)<a$. So this fraction has a smaller numerator than the one we had. So this is a contradiction.
 A: It is a well-known  proof. Essentially it uses denominator descent by the division algorithm, though that is greatly obfuscated. Below I clarify this viewpoint for the generalization below. The proof in the question is exactly the special case $\, k = 2\,$ and $\,q = \lfloor \sqrt 2\rfloor = 1\,$ in the proof below.

Irrationality of $\sqrt k\,$ if it is not an integer  (excerpted from Wikipedia, slightly edited)
For an integer $k>0$, suppose $\sqrt k$ is not an integer, but is rational and can be expressed as $\frac{a}b$ for natural numbers $a$ and $b$, and let $q$ be the largest integer no greater than $\sqrt k.\,$ Then
\begin{aligned}
{\sqrt {k}}
\,&={\frac {a}{b}}={\frac {a({\sqrt {k}}-q)}{b({\sqrt {k}}-q)}}\\[3pt]
&={\frac {a{\sqrt {k}}-aq}{b{\sqrt {k}}-bq}}\\[3pt]
&={\frac {(b{\sqrt {k}}){\sqrt {k}}-aq}{b({\frac {a}{b}})-bq}}\\[3pt]
&={\frac {bk-aq}{\color{#c00}{a-bq}}}\end{aligned}
The numerator and denominator were each multiplied by $(\sqrt k − q)\,$ — which is positive but less than $1$ and then simplified independently. So the two resulting products, say $a'$ and $b'$, are themselves integers, which are less than $a$ and $b$ respectively. Therefore, no matter what natural numbers $a$ and $b$ are used to express $\sqrt k$, there exist smaller natural numbers $a' < a$ and $b' < b$ that have the same ratio. But infinite descent on the natural numbers is impossible, so this disproves the original assumption that $\sqrt k$ could be expressed as a ratio of natural numbers.

We can rewrite the above proof much more conceptually as below, where "$n\,$ is a denom of $\,r$" means that the rational $\,r\,$ is writable with denominator $\,n,\,$ i.e. $\,n\,r = j\,$ for some integer $\,j.$
$$\begin{align}
[\![1]\!]\qquad\quad\:\!\ \  b \sqrt k\, &=\, a\qquad\ \, \Rightarrow \text{$\,b\ $ is a denom of }\:\! \sqrt k\\
\sqrt k\,\cdot\, [\![1]\!]\ \ \, \Rightarrow\,[\![2]\!]\qquad\quad\ \   a\sqrt k\, &=\, bk\qquad  \Rightarrow \text{ $a\,$ is a denom of }\:\! \sqrt k\\
[\![2]\!] - [\![1]\!]\:\!q\,\Rightarrow\,[\![3]\!]  \ \ \ \, (\color{#c00}{a\!-\!bq})\sqrt k\, &=\, bk\!-\!aq\,\Rightarrow\,  \color{#c00}{\bar a} \, \text{ is a denom of $\:\!\sqrt k,\,\ \color{#c00}{\bar a := a\bmod b}$}\\
\end{align}\quad$$
If  $\,b\,$ doesn't divide $\,a\,$ we get a smaller denom $\, 0 < \color{#c00}{a \bmod b} < b\,$ so infinite descent (on denoms), contra $\Bbb N\,$ is well-ordered. Hence $\,b\,$ divides $\,a,\,$ so $\,\sqrt k = a/b = n\in \Bbb Z,\,$ so  $\,k = n^2$.
Alternatively we can use the minimal criminal form of descent: assume that $\,b\,$ is the least denominator then deduce a contradiction that a smaller denominator exists if $\,b\,$ doesn't divide $\,a$.
The denominator descent ($a,b$ denoms $\Rightarrow a\bmod b\,$ denom) can also be performed by taking fractional parts of equivalent fractions (a form favored by John Conway).
Or we can descend quicker via: $\,a,b$ denoms $\Rightarrow \gcd(a,b)=1$ denom, or more simply (but slower) via: $\,a>b$ denoms $\Rightarrow a-b\,$ denom, as explained here, along with generalizations.
This method generalizes to show the $\,\Bbb Z\,$ (or any PID) is integrally-closed, i.e. no proper fraction is a root of a polynomial that is monic (lead coef $= 1),\,$ i.e. the monic case of the Rational Root Test - see my discussion with Gerry Myerson in the Remark here. You can find much further discussion of this and related ideas in my posts on denominator ideals.
