for n, m being Nat ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n by NAT_D:68;