for mlow, mhigh, f being Integer st mhigh < mlow + f & f > 0 holds
ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f )