for a, b being Nat ex m, n being Integer st a gcd b = (a * m) + (b * n)