// Add here the predicates and lemmas needed by your proof

int gcd(int a, int b) {
  // The result should be the GCD of a and b

  while (a != b) {

    if (a < b) {
      b -= a;
    } else {
      a -= b;
    }
  }
  return a;
}