for a being Nat st a is odd holds
ex b being Nat st (a |^ 2) + (b |^ 2) = (b + 1) |^ 2