euclidean algorithm
Let $$m , n \in \mathbb{N}_{1}$$ such that $$m > n$$, if $$m ~\%~ n > 0$$, then $$\gcd{\left ( m , n \right )} = \gcd{\left ( n , m ~\%~ n \right )}$$. Otherwise if $$m ~\%~ n = 0$$, then $$n | m$$ and $$\gcd{\left ( m , n \right )} = n$$

If $$m ~\%~ n = 0$$, then $$m = \left ( m / / n \right ) \cdot n$$, therefore $$\gcd{\left ( m , n \right )} = \gcd{\left ( \left ( m / / n \right ) \cdot n , n \right )} = n$$, so now assume that $$m ~\%~ n > 0$$

Recall that $$m = \left ( m / / n \right ) \cdot n + m ~\%~ n$$, therefore $$m - \left ( m / / n \right ) \cdot n = m ~\%~ n$$, so that if $$d$$ divides both $$m , n$$, then it must divide $$m ~\%~ n$$ (and clearly $$n$$), and by the original equation if $$d$$ is a divisor of both $$n , m ~\%~ n$$ then $$d$$ divides $$m$$ (and clearly $$n$$).

The above paragraph shows that a number is a divisor of $$m , n$$ if and only if it is a divisor of $$n , m ~\%~ n$$, which shows that their set of divisors are equal and thus $$\gcd{\left ( m , n \right )} = \gcd{\left ( n , m ~\%~ n \right )}$$

bounded sum implies one less then half
Suppose that $$x , y , b \in \mathbb{N}_{1}$$ and $$x < y$$ with $$x + y \le b$$, then $$x < \frac{b}{2}$$
Suppose for the sake of contradiction that $$x \ge \frac{b}{2}$$, then we know that $$y > x \ge \frac{b}{2}$$ so therefore $$x + y \gt \frac{b}{2} + \frac{b}{2} = b$$, so we have $$x + y > b$$ which is a contradiction so that $$x < \frac{b}{2}$$.
euclidean algorithm has exponentially decreasing remainders
Let $$a , b \in \mathbb{N}_{1}$$ with $$a \ge b$$ be two integers, and suppose we will preform the euclidean algorithm on them to compute $$\gcd{\left ( m , n \right )}$$, supposing that $$r_{k}$$ represents the remainder after $$k$$ (where $$k \in \mathbb{N}_{1}$$) steps into the euclidean algorithm, then $$r_{2 n} \lt \frac{b}{2^{n}}$$

For the base case, suppose that $$n = 1$$, so we'd like to prove that $$r_{2} \lt \frac{b}{2}$$. Firstly we know that $$a = b q_{0} + r_{0}$$ with $$0 \le r_{0} \lt b$$, then applying the next iteration we have $$b = r_{0} q_{1} + r_{1}$$ with $$0 \le r_{1} \lt r_{0}$$ and one more time, we get $$r_{0} = r_{1} q_{2} + r_{2}$$ with $$0 \le r_{2} \lt r_{1}$$, this shows us that $$b = \left ( r_{1} q_{2} + r_{2} \right ) q_{1} + r_{1}$$.

Since $$a \ge b$$, $$b \gt r_{0}$$ and $$r_{0} \gt r_{1}$$, then $$q_{0} \ge 1$$, $$q_{1} \ge 1$$ and $$q_{2} \ge 1$$, therefore $$b = \left ( r_{1} q_{2} + r_{2} \right ) q_{1} + r_{1} \ge \left ( r_{1} \cdot 1 + r_{2} \right ) \cdot 1 + r_{1} \ge r 1 + r 2$$ therefore $$r_{2} < \frac{b}{2}$$ which concludes the base case

Now let $$k \in \mathbb{N}_{1}$$ assuming that $$r_{2 k} \le \frac{b}{2^{k}}$$, we want to prove that $$r_{2 \left ( k + 1 \right )} = \frac{b}{2^{k + 1}}$$, noting that $$2 \left ( k + 1 \right ) = 2 k + 2$$.

To start let's say we have an intance of the euclidean algorithm that lasts for at least $$2 k + 2$$ iterations, therefore we know that $$r_{2 k} \le \frac{b}{2^{k}}$$ by our induction hypothesis, additionally at the $$2 k$$-th iteration we would have an equation of the form $$r_{2 k} = r_{2 k + 1} \left ( q_{2 k + 2} \right ) + r_{2 k + 2}$$, since we know that $$r_{2 k + 1} > r_{2 k + 2}$$, then $$q_{2 k + 2} \ge 1$$, which then shows that $$r_{2 k} = r_{2 k + 1} \left ( q_{2 k + 2} \right ) + r_{2 k + 2} \ge r_{2 k + 1} + r_{2 k + 1}$$, and since $$\frac{b}{2^{k}} \gt r_{2 k}$$ , then we know that $$r_{2 k + 2} \lt \frac{1}{2} \cdot \frac{b}{2^{k}} = \frac{b}{2^{k + 1}}$$ which is what we needed to show

upper bound on euclidean algorithm iterations
The euclidean algorithm terminates in at most $$2 \log_{2}{\left ( b \right )}$$ iterations
The euclidean algorithm terminates in $$k$$ iterations if and only if $$r_{k} = 0$$, we know that for all $$n \in \mathbb{N}_{1}$$ that $$r_{2 n} \lt \frac{b}{2^{n}}$$, therefore when $$n = \log_{2}{\left ( b \right )}$$, then we have $$r_{2 \log_{2}{\left ( b \right )}} \lt \frac{b}{2^{\log_{2}{\left ( b \right )}}} = \frac{b}{b} = 1$$, but if $$r_{2 \log_{2}{\left ( b \right )}} \lt 1$$, then since the remainders are always elements of $$\mathbb{N}_{0}$$, then we know that $$r_{2 \log_{2}{\left ( b \right )}} = 0$$, thus we've shown after $$2 \log_{2}{\left ( b \right )}$$ iterations the algorithm must terminate