theorem :: PREPOWER:97

for a, b being Integer st a >= 0 & b >= 0 holds
a gcd b = a gcd (b - a)