theorem Th32: :: BINARI_3:32

for n being non zero Nat
for k being Nat st k + 1 < 2 to_power n holds
add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE