for a, x, k being Nat st k > 0 & x divides a + k & x divides a - k holds
x <= 2 * k