for n being Element of NAT holds [/(n / 2)\] <= n by Lm17;