( 0 < b & b < 1 ) by COMPLEX3:1;
then ( (a - b) + 0 < (a - b) + b & (a - b) + b < (a - b) + 1 ) by XREAL_1:6;
hence [/(a - b)\] = a by INT_1:def 7; :: thesis: verum