for n being Nat st n >= 1 holds
n -' 1 <= (2 * n) -' 2