let a, b, x be Nat; :: thesis: ( x > 0 & (a |^ 2) + (b |^ 2) = (b + 1) |^ 2 implies (a |^ 2) + ((b - x) |^ 2) > ((b + 1) - x) |^ 2 )
A0: b + 1 > b + 0 by XREAL_1:6;
assume A1: ( x > 0 & (a |^ 2) + (b |^ 2) = (b + 1) |^ 2 ) ; :: thesis: (a |^ 2) + ((b - x) |^ 2) > ((b + 1) - x) |^ 2
consider q being Integer such that
A2: q = - x ;
(a |^ 2) + ((b + q) |^ 2) > ((b + 1) + q) |^ 2 by A0, A1, A2, Th44;
hence (a |^ 2) + ((b - x) |^ 2) > ((b + 1) - x) |^ 2 by A2; :: thesis: verum