for k, m, n being Integer holds
( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )