let r, s be real number ; :: thesis: ( r >= s implies [\r/] >= [\s/] )
assume A1: r >= s ; :: thesis: [\r/] >= [\s/]
assume [\r/] < [\s/] ; :: thesis: contradiction
then A2: [\r/] + 1 <= [\s/] by INT_1:20;
r - 1 < [\r/] by INT_1:def 4;
then (r - 1) + 1 < [\r/] + 1 by XREAL_1:8;
then ( r < [\s/] & [\s/] <= s ) by A2, INT_1:def 4, XXREAL_0:2;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum