for n being non zero Nat holds
( 0 <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= 0 )