let r, s be Real; :: thesis: ( 0 <= r & r < s implies [\(r / s)/] = 0 )
assume A1: ( 0 <= r & r < s ) ; :: thesis: [\(r / s)/] = 0
then r / s < s / s by XREAL_1:74;
then (r / s) - 1 < (s / s) - 1 by XREAL_1:9;
then (r / s) - 1 < 1 - 1 by A1, XCMPLX_1:60;
hence [\(r / s)/] = 0 by A1, INT_1:def 6; :: thesis: verum