let mlow, mhigh, f be Integer; :: thesis: ( mhigh < mlow + f & f > 0 implies ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f ) )
assume A1: ( mhigh < mlow + f & f > 0 ) ; :: thesis: ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f )
then reconsider f = f as Element of NAT by INT_1:16;
A2: mhigh mod f = mhigh - ((mhigh div f) * f) by A1, INT_1:def 8;
then A3: mhigh - ((mhigh div f) * f) < f by A1, INT_3:9;
A4: 0 <= mhigh - ((mhigh div f) * f) by A1, A2, INT_3:9;
mhigh + (- ((mhigh div f) * f)) < (mlow + f) + (- ((mhigh div f) * f)) by A1, XREAL_1:8;
then 0 + (- f) < ((mlow + (- ((mhigh div f) * f))) + f) + (- f) by A4, XREAL_1:8;
then - f < mlow - ((mhigh div f) * f) ;
hence ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f ) by A3; :: thesis: verum