$\varepsilon$-orders satisfy Ho's identity $(\ast)$

For every $\varepsilon$, all integers $a$ and all $r\neq0$,

This is the $\mathbb{Z}$-version of identity (1) in Ho's paper ($a\triangleleft b\iff c\triangleleft d$ for a $4$-term progression $a,b,c,d$), which drives both of Ho's lemmas.

Formalization Note epsLt ε x y is x ≠ y ∧ (x / 2^k % 2 = 1 ↔ ε k = true) with k = padicValInt 2 (y - x), i.e. $k=\nu_2(y-x)$; integer division is floor division, so x / 2^k % 2 is the $k$-th two's-complement digit of $x$.