theorem FLM: :: NUMERAL3:8

for a being non integer Real holds [\a/] + [\(- a)/] = - 1