let a, b, m be Integer; :: thesis: ( a < b implies ex k being Nat st
( m < (((b - a) * k) + 1) - a & k = |.[/((((m + a) - 1) / (b - a)) + 1)\].| ) )
assume a < b ; :: thesis: ex k being Nat st
( m < (((b - a) * k) + 1) - a & k = |.[/((((m + a) - 1) / (b - a)) + 1)\].| )
then A1: a - a < b - a by XREAL_1:14;
set x = (((m + a) - 1) / (b - a)) + 1;
A2: ((b - a) * ((((m + a) - 1) / (b - a)) + 1)) / (b - a) = (((m + a) - 1) / (b - a)) + 1 by A1, XCMPLX_1:89;

A3: now :: thesis: not m >= (((b - a) * ((((m + a) - 1) / (b - a)) + 1)) + 1) - a

assume m >= (((b - a) * ((((m + a) - 1) / (b - a)) + 1)) + 1) - a ; :: thesis: contradiction
then m + a >= ((((b - a) * ((((m + a) - 1) / (b - a)) + 1)) + 1) - a) + a by XREAL_1:6;
then (m + a) - 1 >= (((b - a) * ((((m + a) - 1) / (b - a)) + 1)) + 1) - 1 by XREAL_1:9;
then ((m + a) - 1) / (b - a) >= ((((m + a) - 1) / (b - a)) + 1) + 0 by A1, A2, XREAL_1:72;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

take k = |.[/((((m + a) - 1) / (b - a)) + 1)\].|; :: thesis: ( m < (((b - a) * k) + 1) - a & k = |.[/((((m + a) - 1) / (b - a)) + 1)\].| )
A4: (((m + a) - 1) / (b - a)) + 1 <= [/((((m + a) - 1) / (b - a)) + 1)\] by INT_1:def 7;
[/((((m + a) - 1) / (b - a)) + 1)\] <= k by ABSVALUE:4;
then (((m + a) - 1) / (b - a)) + 1 <= k by A4, XXREAL_0:2;
then (b - a) * ((((m + a) - 1) / (b - a)) + 1) <= (b - a) * k by A1, XREAL_1:64;
then ((b - a) * ((((m + a) - 1) / (b - a)) + 1)) + 1 <= ((b - a) * k) + 1 by XREAL_1:6;
then (((b - a) * ((((m + a) - 1) / (b - a)) + 1)) + 1) - a <= (((b - a) * k) + 1) - a by XREAL_1:9;
hence ( m < (((b - a) * k) + 1) - a & k = |.[/((((m + a) - 1) / (b - a)) + 1)\].| ) by A3, XXREAL_0:2; :: thesis: verum