let n be non empty 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 A1: ( ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & 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 A1, INT_3:12;
hence 2sComplement n,h = 2sComplement n,i by A1, Lm5, Lm6; :: thesis: verum