for n being Nat st n >= 2 holds
[/(n / 2)\] < n by Lm46;