Well, x mod 1 is just x minus a series of Heaviside step functions, each of which are non-constructive. The core problem is determining if your real number x is equal to an integer. You might be able to prove that x is close to a particular n, but there may not be a constructive proof of either x<n, x=n, or x>n. Hence you don't know if x mod 1 should be x-(n-1) or x-n.