## The greatest common divisor of two natural numbers

Context gcd

uses builtins/integers

The greatest common divisor gcd(a:ℕ, b:ℕ) : ℕ of two natural numbers a:ℕ and b:ℕ can be obtained by applying the following rules:

If the two numbers are equal, their GCD is equal to them as well:

gcd(a, a) ⇒ aIf a > b, replace a by a-b:

gcd(a, b) ⇒ gcd(a - b, b) if a > bOtherwise we have b > a and replace b by b-a:

gcd(a, b) ⇒ gcd(a, b - a)

Here are some application examples:

gcd(2, 3) ⇒ 1

gcd(3, 2) ⇒ 1

gcd(42, 7) ⇒ 7