let n be non empty Nat; :: thesis: for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds
n -BinarySequence l = n -BinarySequence m
let l, m be Nat; :: thesis: ( l mod (2 to_power n) = m mod (2 to_power n) implies n -BinarySequence l = n -BinarySequence m )
assume A1: l mod (2 to_power n) = m mod (2 to_power n) ; :: thesis: n -BinarySequence l = n -BinarySequence m
abs m = m by ABSVALUE:def 1;
then A2: 2sComplement n,m = n -BinarySequence m by Def2;
abs l = l by ABSVALUE:def 1;
then 2sComplement n,l = n -BinarySequence l by Def2;
hence n -BinarySequence l = n -BinarySequence m by A1, A2, Lm5; :: thesis: verum