theorem :: BINARI_4:37

for h, i being Integer
for n being non zero Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i