theorem :: BINARI_4:29

for n being non zero Nat
for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n holds
2sComplement (n,h) = 2sComplement (n,i)