theorem :: NTALGO_1:2

for a, b being Element of INT holds ALGO_GCD (a,b) = a gcd b