Proof:Gcd(a,b) is a common divisor of a and b

Definition: gcd

Euclid's GCD algorithm is the function which is given as follows: , and for , where .

This function is a good inductively defined function because by definition, , so the second argument is decreasing in the inductive definition.

The algorithm can be extended to operate on negative integers by simply taking the gcd of the absolute values of its arguments.

Claim (see proof):

For all , and

Proof:

We will do this proof by induction. Since the inductive principle used to define uses strong induction on the second argument, we will use the same inductive principle for the proof. Let be the statement "for all , and ". We will prove and assuming for all .

To see , we want to show that and . Note that by definition, . because [math]1 \cdot a = a [/math], and because [math]0 \cdot a = 0 [/math].

Now, to see , assume for all [math]k \lt b [/math]. To save some writing, let's define , by definition, we have (for simplicity, let's call this number [math]g [/math]); thus we want to show that and .

Now, since , we know [math]r \lt b [/math]. Thus we can apply [math]P(r) [/math] (with [math]b [/math] plugged in for [math]a [/math]), to conclude that and . This gives us one of the two things we need to prove, so all that's left is to show that .

Let's take stock of where we are:

Since we have [math]sg = b [/math] for some [math]s [/math].
We also have [math]tg = r [/math] for some [math]t [/math] since .
We also know [math]a = qb + r [/math] for some [math]q [/math] since .
We want to show that there exists with [math]a = cg [/math].

Combining these equations, we have

Thus, choosing shows as required.