let a be non zero Nat; :: thesis: for b being Nat st b mod a < [/(a / 2)\] holds
frac (b / a) < 1 / 2
let b be Nat; :: thesis: ( b mod a < [/(a / 2)\] implies frac (b / a) < 1 / 2 )
assume A1: b mod a < [/(a / 2)\] ; :: thesis: frac (b / a) < 1 / 2
A2: ( a / 2 <= [/(a / 2)\] & [/(a / 2)\] <= (a / 2) + 1 ) by INT_1:def 7;

per cases ( a is even or a is odd ) ;

suppose a is even ; :: thesis: frac (b / a) < 1 / 2

then reconsider c = a / 2 as non zero Nat ;
B1: (a / 2) / a = (1 / 2) * (a / a) by XCMPLX_1:104
.= (1 / 2) * 1 by XCMPLX_1:60 ;
a * (frac (b / a)) < c by A1, R3;
then a * (frac (b / a)) < a * (c / a) by XCMPLX_1:87;
hence frac (b / a) < 1 / 2 by B1, XREAL_1:64; :: thesis: verum

end;

suppose a is odd ; :: thesis: frac (b / a) < 1 / 2

then reconsider c = (a + 1) / 2 as non zero Nat ;
a - 1 < a - 0 by XREAL_1:10;
then (a - 1) / 2 < a / 2 by XREAL_1:74;
then ((a - 1) / 2) / a < (a / 2) / a by XREAL_1:74;
then (((a + 1) / 2) - 1) / a < (1 / 2) * (a / a) by XCMPLX_1:104;
then B0: (c - 1) / a < (1 / 2) * 1 by XCMPLX_1:60;
B1: ( (a / 2) - (1 / 2) < (a / 2) - 0 & (a / 2) + 0 < (a / 2) + (1 / 2) & ((a / 2) + 1) + 0 < ((a / 2) + 1) + (1 / 2) ) by XREAL_1:10, XREAL_1:6;
then c - 1 < [/(a / 2)\] by A2, XXREAL_0:2;
then B2: (c - 1) + 1 <= [/(a / 2)\] by INT_1:7;
[/(a / 2)\] < c + 1 by B1, A2, XXREAL_0:2;
then [/(a / 2)\] <= c by INT_1:7;
then b mod a < (c - 1) + 1 by A1, B2, XXREAL_0:1;
then b mod a <= c - 1 by INT_1:7;
then a * (frac (b / a)) <= c - 1 by R3;
then a * (frac (b / a)) <= a * ((c - 1) / a) by XCMPLX_1:87;
then frac (b / a) <= (c - 1) / a by XREAL_1:68;
hence frac (b / a) < 1 / 2 by B0, XXREAL_0:2; :: thesis: verum

end;

end;