gcd((i:int), (j:{(jj:int) | (i = 0) = > (jj /= 0)} )): {(k:posnat) | divides(k, i) AND divides(k, j)} = max({(k:posnat) | divides(k, i) AND divides(k, j)});