for n being Element of NAT st n >= 3 holds
2 * (n - 2) >= n - 1 by Lm35;