let a, b be Real; :: thesis: ( a <= b implies [\a/] < [\b/] + 1 )
assume A1: a <= b ; :: thesis: [\a/] < [\b/] + 1
then A2: [/a\] <= [\b/] + 1 by CF2;

per cases ( a is integer or not a is integer ) ;

suppose a is integer ; :: thesis: [\a/] < [\b/] + 1

then reconsider a = a as Integer ;
[\a/] = a ;
hence [\a/] < [\b/] + 1 by A1, INT_1:29, XXREAL_0:2; :: thesis: verum

end;

suppose not a is integer ; :: thesis: [\a/] < [\b/] + 1

hence [\a/] < [\b/] + 1 by A2, XXREAL_0:2, INT_1:35; :: thesis: verum

end;

end;