for a, b, x being Nat st x > 0 & (a |^ 2) + (b |^ 2) = (b + 1) |^ 2 holds
(a |^ 2) + ((b - x) |^ 2) > ((b + 1) - x) |^ 2