:: deftheorem defines are_coprime INT_2:def 3 :
for a, b being Integer holds
( a,b are_coprime iff a gcd b = 1 );