Mapping lexicographical comparison to integer comparison

Claim

(a, b) < (c, d) with a,b,c,d ∈ [0,M) ⇔ a · M + b < c · M + d
(a, b) = (c, d) with a,b,c,d ∈ [0,M) ⇔ a · M + b = c · M + d
(a, b) > (c, d) with a,b,c,d ∈ [0,M) ⇔ a · M + b > c · M + d

Proof by case distinction
relation to prove constraint evaluation conclusion
(a, b) < (c, d) a < c a · M + M – 1 < c · M
(a, b) < (c, d) a = c ∧ b < d a · M + b < c · M + d 0 + b < 0 + d ✓
(a, b) = (c, d) a = c ∧ b = d a · M + b = c · M + d 0 + 0 = 0 + 0 ✓
(a, b) > (c, d) a = c ∧ b > d a · M + b > c · M + d 0 + b > 0 + d ✓
(a, b) > (c, d) a > c a · M > c · M + M – 1
Rationale

This just exploits the nature of a lexicographical order itself for bounded domains. Consider two binary numbers and they get compared. This integer comparison equals the lexicographical tuple comparison of its digit expansion. I just wanted to make this explicit as my head was screwing around with it.

Mapping lexicographical comparison to integer comparison