let a, b be Real; :: thesis: ( a <= b implies [/a\] <= [\b/] + 1 )
assume a <= b ; :: thesis: [/a\] <= [\b/] + 1
then A2: ( [\a/] <= [\b/] & [/a\] <= [/b\] ) by PRE_FF:9;
[/b\] <= [\b/] + 1 by CF1;
hence [/a\] <= [\b/] + 1 by A2, XXREAL_0:2; :: thesis: verum