for s being non trivial Nat
for x being b₁ -gonal number holds 0 <= (((8 * s) - 16) * x) + ((s - 4) ^2)