for m, n being Element of NAT holds
( not m,n are_coprime or m > 0 or n > 0 )