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 by INT_1:30; :: 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;