theorem :: NEWTON06:11

for a being non integer Real holds
( - 1 < (frac a) - (frac (- a)) & (frac a) - (frac (- a)) < 1 )