The greatest common divisor of two natural numbers

The greatest common divisor of two natural numbers

Euclid

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:
  1. If the two numbers are equal, their GCD is equal to them as well:
    gcd(a, a) ⇒ a

  2. If a > b, replace a by a-b:
    gcd(a, b) ⇒ gcd(a - b, b)  if a > b

  3. Otherwise 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