Proving correctness of Euclid's GCD Algorithm through Induction So I'm completely stuck on how to prove Euclid's GCD Algorithm, given that we know the theorem $\texttt{gcd}(a, b) = \texttt{gcd}(b, a -b)$ as well as $\texttt{gcd}(a, b) = (b, a \bmod b)$
How would we go about proving the correctness of the algorithm, essentially that the GCD returned call it $d$, by $\texttt{gcd}(a, b)$ is correct for all pairs of $(a, b)$? 
My instinct is to use induction, but I don't quite understand what we would be using induction on.. I find the two theorems straightforward, but I don't quite understand how to apply them in a manner to begin an induction proof (I'm thinking strong induction) to show that the algorithm correctly computes the GCD for all pairs $(a, b)$ such that $a \in \mathbb{N}$, $b \in \mathbb{N}$ and $a > b$ since if $b > a$ the algorithm will simply switch the two. 
I've referred to the CLRS book where they provide proofs of the theorems (but I understand the theorems and don't have to prove these) but am still completely stuck on how to move forward. I imagined starting with some base case such as $$gcd(1,0)$$ or $$gcd(2, 0)$$ or $$gcd(2, 1)$$ but from there I'm not sure what we're using induction on, or what the inductive step really would be. I understand we basically have to show that the algorithm gets down to our base case, that is $a \bmod b $ is $0$, the last remainder stored by the function is returned and that is our gcd. 
I also went through some examples with numbers, like $gcd(55, 34)$ and continuously applied the theorem that $gcd(a, b) = gcd(b, a - b)$ to see that the recursive call finally ends in $gcd(1, 1)$ and $1 \bmod 1$ = $0$, so $1$ is returned. 
Could someone please shed some light on how to move forward? Have spent significant time trying to attempt this proof. 
 A: The key here, quoting from the section Infinite descent in the wikipedia article on mathematical induction, is
$\quad$ ... there are no infinite decreasing sequences of natural numbers
Here we provide constructions/hints and leave the organization/exposition of the theory to the interested reader.
Recall that we have the first projection mapping $\pi_1$ on $\Bbb Z^{+} \times \Bbb Z^{+}$ defined by:
$\quad \forall \, (m,m) \in \Bbb Z^{+} \times \Bbb Z^{+} : \pi_1(m,n)=m$
Define $P = \{ (m,n) \in \Bbb Z^{+} \times \Bbb Z^{+} \mid m \ge n \} $. Recall that the set $P$ contains the diagonal set
$\quad \quad \quad \Delta_{\mathbb Z^{+}} = \{(d,d) \mid d \in \mathbb Z^{+}\}$.
We define the function $F: P \to P$ as follows
$$   
    F(m,n) = \left\{\begin{array}{lr}
        (m,n)  & \text{if } m = n\\
        (m-n,n)  & \text{if } m-n \ge n\\
        (n,m-n)  & \text{if } m-n \lt n\\
        \end{array}\right\} 
$$ 
If $(m,n) \in P$ we can apply the $\text{gcd}$ function. Note that for elements $(d,d)$ in the diagonal $\Delta_{\mathbb Z^{+}}$,
$\tag 1 \text{gcd}(d,d) = d$
Now it is well known that
$\tag 2 \text{gcd}(m,n) = \text{gcd}\big(F(m,n)\big)$
For fixed $(s,t)$ in the domain of $F$ we define a sequence
$\tag 3 a_k = \pi_1 \circ F^k(s,t)$
By using the absurdity of an infinite descent, the sequence $(a_k)$ eventually 'stops decreasing and remains constant. That happens precisely when the algorithm $F$ 'hits the diagonal.
So the algorithm $F$ 'gets us' to the diagonal in a finite number of steps, and from there we can just 'read off' greatest common divisor.

Example: Let $m = 28$ and $n = 10$ so that $(m,n)$ belongs to the domain of $F$.
$\quad F(28,10) = (18, 10)$
$\quad F(18,10) = (10, 8)$
$\quad F(10,8) = (8, 2)$
$\quad F(8,2) = (6, 2)$
$\quad F(6,2) = (4, 2)$
$\quad F(4,2) = (2, 2)$ STOP
Of course if you don't want to stop you can continue to apply $F$. But the points on the diagonal are exactly the fixed points of $F$, so you will quickly lose interest.
The point $(2,2) \in \Delta_{\mathbb Z^{+}}$ and so $\text{gcd}(28,10) = 2$.
A: Hint Use (strong) induction on $a+b$. Note that $(a-qb)+b<a+b$ as long as $q \neq 0$, which is always the case when you divide the largest number by the smallest, i.e. $a \geq b$. 
A: Here we give a complete proofs accepting the following as true,
Proposition 1: For any two distinct integers $a,b \in \Bbb Z^{+}$ with $a \gt b$,
$\tag 1  \text{gcd}(a,b) =  \text{gcd}(a-b,b)$
Define $P = \{ (m,n) \in \Bbb Z^{+} \times \Bbb Z^{+} \mid m \ge n \} $. Recall that the set $P$ contains the diagonal set
$\quad \quad \quad \Delta_{\mathbb Z^{+}} = \{(d,d) \mid d \in \mathbb Z^{+}\}$.
To avoid any confusion define the function $G: P \to \mathbb Z^{+}$ as follows
$\tag 2 (a,b) \mapsto  \text{gcd}(a,b)$
Note that no calculations are necessary to compute $G(z)$ when $z \in \Delta_{\mathbb Z^{+}}$.
We also define the function $F: P \to P$ as follows
$$\tag 3   
    F(a,b) = \left\{\begin{array}{lr}
        (a,b)  & \text{if } a = b\\
        (a-b,b)  & \text{if } a-b \ge b\\
        (b,a-b)  & \text{if } a-b \lt b\\
        \end{array}\right\} 
$$ 
Note that a point $z \in P$ is a fixed point of the function $F$ if and only if $z \in \Delta_{\mathbb Z^{+}}$.
Proposition 2: For every $z \in P$ and integer $k \ge 1$ the following holds
$\tag 4 G(z) = G(F^k(z))$
Proof
We prove the proposition using simple induction.
Base Case $k=1$:
If $z \in \Delta_{\mathbb Z^{+}}$ then obviously $G(z) = G(F(z))$.
Otherwise, we simply translate proposition 1 to this setting.
Step Case: Assume $\text{(4)}$ is true.
If $F^k(z) \in \Delta_{\mathbb Z^{+}}$ then $G(F^{k+1}(z)) = G(F^{k}(z)) = G(z)$, so that has been addressed.
Otherwise, we simply translate proposition 1 to this setting while using the transitivity property of the equality relation. $\quad \blacksquare$
Proposition 3: For every $z \in P$ there exist a $k \ge 1$ such that $F^k(z) \in \Delta_{\mathbb Z^{+}}$.
Proof
We shall use Fermat's method of descent.
Assume the statement
$\tag 5 Q(n) : n := a + b \land (a,b) \in P \land [\forall k \ge 1, \, F^k(a,b) \notin \Delta_{\mathbb Z^{+}}]$
is true.
Letting $\pi_1$ and $\pi_2$ denote the first and second projection mappings defined on  $\mathbb Z^{+} \times \mathbb Z^{+}$ (see definitions here), we define
$\quad a' = \pi_1(F(a,b)) \text{ and } b' = \pi_2(F(a,b))$
and can then write as true
$\tag 6 Q(m) : m := a' + b' \land (a',b') \in P \land [\forall k \ge 1, \, F^k(a',b') \notin \Delta_{\mathbb Z^{+}}]$
where $m \lt n$.
By reductio ad absurdum, $\text{(5)}$ must rejected.  $\quad \blacksquare$
