theorem :: NEWTON06:12

for a being non integer Real holds
( frac a = frac (- a) iff 2 * a is odd Integer )