let a, r be real number ; :: thesis: ( a >= [\r/] + 1 & a <= r + 1 implies [\a/] = [\r/] + 1 )
assume A1: a >= [\r/] + 1 ; :: thesis: ( not a <= r + 1 or [\a/] = [\r/] + 1 )
assume a <= r + 1 ; :: thesis: [\a/] = [\r/] + 1
then a - 1 <= (r + 1) - 1 by XREAL_1:11;
then a - 1 < [\r/] + 1 by INT_1:52, XXREAL_0:2;
hence [\a/] = [\r/] + 1 by A1, INT_1:def 4; :: thesis: verum