theorem Th24: :: HILB10_1:21
for x being Integer
for a being non trivial Nat st x <= 0 holds
(sgn x) * (Py (a,|.x.|)) = - (Py (a,|.x.|))