theorem Th35: :: BINARI_4:35

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