theorem :: BINARI_4:36

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