Proof of Bezout's Lemma using Euclid's Algorithm backwards

Below is a simple conceptual proof of Bezout's identity for the gcd.

The set $\rm\:S\:$ of all integers of form $\rm\:a\:x + b\:y,\,\ x,y\in \mathbb Z,\:$ is closed under subtraction so, by Lemma below, every positive $\rm\:n\in S\:$ is divisible by $\rm\:d = $ least positive $\rm\in S,\:$ so $\rm\:a,b\in S\:$ $\Rightarrow$ $\rm\:d\:|\:a,b.\:$ Thus $\rm\:d\:$ is a common divisor of $\rm\:a,b,\:$ necessarily greatest, $ $ by $\rm\:c\:|\:a,b\:$ $\Rightarrow$ $\rm\:c\:|\:d = a\:x\!+\! b\:y\:$ $\Rightarrow$ $\rm\:c\le d.$

Lemma $\ $ If a nonempty set of positive integers $\rm\: S\:$ satisfies both $\rm\ n > m\: \in\, S \ \Rightarrow\ n-m\, \in\, S$
then every element of $\rm\:S\:$ is a multiple of the least element $\rm\:m_{\circ} \in\, S.$

Proof $\,\bf 1$ $\ $ If not there is a least nonmultiple $\rm\:n\in S,\,$ contra $\rm\:n-m_{\circ} \in S\:$ is a nonmultiple of $\rm\:m_{\circ}$

Proof $\,\bf 2$ $\rm\ \ S\,$ closed under subtraction $\rm\:\Rightarrow\:S\,$ closed under remainder (mod), when it is $\ne 0,$ since mod may be computed by repeated subtraction, i.e. $\rm\: a\ mod\ b\, =\, a - k b\, =\, a-b-b-\cdots -b.\:$ Hence $\rm\:n\in S\:$ $\Rightarrow$ $\rm\: n\ mod\ m_\circ = 0,\:$ else it is $\rm\,\in S\,$ and smaller than $\rm\:m_\circ\,$ contra mimimality of $\rm\:m_\circ$

Remark $\ $ In a nutshell, two applications of induction yield the following inferences

$$\!\rm\begin{eqnarray} S\ closed\ under\ subtraction &\!\Rightarrow\:&\rm S\ closed\ under\ mod \!=\! remainder = repeated\ subtraction \\ &\!\Rightarrow\:&\rm S\ closed\ under\ gcd\! =\! repeated\ remainder\!\!: Euclid'\!s\ algorithm \end{eqnarray}$$

Interpreted constructively, this yields the extended Euclidean algorithm for the gcd. Namely, $ $ starting from the two elements of $\rm\,S\,$ that we know: $\rm\ a \,=\, 1\cdot a + 0\cdot b,\ \ b \,=\, 0\cdot a + 1\cdot b,\ $ we search for the least element of $\rm\,S\,$ by repeatedly subtracting elements to produce smaller elements of $\rm\,S\,$ (while keeping track of every elements linear representation in terms of $\rm\,a\,$ and $\rm\,b).\:$ This is essentially the subtractive form of the Euclidean algorithm (vs. the mod/remainder form).