theorem :: ASYMPT_1:75

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