theorem Th27: :: WSIERP_1:27

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