Naturally, this proof only works for arbitrary-precision integers: when you use fixed-precision integers, the algorithm will wrongfully report "false" for arrays like e.g. [INT_MIN, -1] or (if you insist on C semantics) [UINT_MAX, 1].
Hopefully the proof would break if one tried to transfer it over?
Hopefully the proof would break if one tried to transfer it over?