theorem :: NUMBER08:104

for x, y being positive Nat holds not x * (x + 1) = (4 * y) * (y + 1)