theorem :: NAT_D:68
for a, b being Integer ex s, t being Integer st a gcd b = (s * a) + (t * b)