n > 0 be a natural number and for any two reminders
a, b modulo
2^n we have that
a < b iff
a xor 0x800..00 <(signed) b xor 0x800...00.
It is also true that
a <(signed) b iff
(0x800...00 & b <= 0x800...00 & a) && (a & 0x7FF...FFF < b & 0x7FF...FFF).
Is there a way to prove the equivalence of these two propositions?