let
def x = sub (
Q
.from_z (ceil x)) x