for m, n being Nat st m,n are_coprime holds
for k being Nat ex i, j being Integer st (i * m) + (j * n) = k