theorem Th14: :: NUMBER03:14

for i, j being Integer holds
( not i,j are_coprime or i <> j or ( i = j & j = 1 ) or ( i = j & j = - 1 ) )