for m being Nat holds 2 to_power m >= m