let n be Nat; :: thesis: [/(n / 2)\] <= n

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: [/(n / 2)\] <= n

hence [/(n / 2)\] <= n ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: [/(n / 2)\] <= n

then A1: n >= 0 + 1 by NAT_1:13;

per cases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;

suppose A2: n = 1 ; :: thesis: [/(n / 2)\] <= n

now :: thesis: not [/(1 / 2)\] > 1

assume [/(1 / 2)\] > 1 ; :: thesis: contradiction
then A3: [/(1 / 2)\] >= 1 + 1 by INT_1:7;
[/(1 / 2)\] < (1 / 2) + 1 by INT_1:def 7;
hence contradiction by A3, XXREAL_0:2; :: thesis: verum

end;

hence [/(n / 2)\] <= n by A2; :: thesis: verum

end;

suppose n > 1 ; :: thesis: [/(n / 2)\] <= n

then A4: n >= 1 + 1 by NAT_1:13;

A5: now :: thesis: not (n / 2) + 1 > n

assume (n / 2) + 1 > n ; :: thesis: contradiction
then 2 * ((n / 2) + 1) > 2 * n by XREAL_1:68;
then (2 * (n / 2)) + (2 * 1) > 2 * n ;
then 2 > (2 * n) - n by XREAL_1:19;
hence contradiction by A4; :: thesis: verum

end;

[/(n / 2)\] < (n / 2) + 1 by INT_1:def 7;
hence [/(n / 2)\] <= n by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;