theorem :: NUMBER03:15

for i, j being Nat holds
( not i,j are_coprime or i <> j or ( i = j & j = 1 ) ) by Th14;