let n be non zero Nat; :: thesis: 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)
let h, i be Integer; :: thesis: ( ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n implies 2sComplement (n,h) = 2sComplement (n,i) )
assume that
A1: ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) and
A2: h,i are_congruent_mod 2 to_power n ; :: thesis: 2sComplement (n,h) = 2sComplement (n,i)
h mod (2 to_power n) = i mod (2 to_power n) by A2, NAT_D:64;
hence 2sComplement (n,h) = 2sComplement (n,i) by A1, Lm5, Lm6; :: thesis: verum