theorem :: NUMBER08:109

for k, x, y being Nat st (x ^2) - (2 * (y ^2)) = k holds
for t, u being Nat st t = x - (2 * y) & u = x - y holds
(t ^2) - (2 * (u ^2)) = - k ;