theorem :: BINARI_4:28

for n being non zero Nat
for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement (n,h) = 2sComplement (n,i) by Lm5, Lm6;