theorem :: NEWTON02:71

for a, b being Nat
for t being Integer st b |^ 2 = ((2 * a) + t) * t holds
ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2