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.

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 , and because .

Now, to see , assume for all . To save some writing, let's define , by definition, we have (for simplicity, let's call this number ); thus we want to show that and .

Now, since , we know . Thus we can apply (with plugged in for ), 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:

Combining these equations, we have

Thus, choosing shows as required.