theorem :: NEWTON02:70

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