[quickthrower2]

You need refinement types. Psuedocode:

    timespandays : int, timespandays > 0

your program can then be proven by the compiler not to NaN.