theorem :: NUMBER14:12

for i, j being Integer holds
( i,j are_coprime iff - i,j are_coprime ) by NEWTON02:1;