theorem FRA: :: NEWTON06:10

for a being non integer Real holds (frac a) + (frac (- a)) = 1