 The natural order relation \(x \lt y\) can be defined in \(\mathbf{HA}\) by \(\exists z(S(z) + x = y),\) or by the quantifier-free formula \(S(x) \dot{-} y = 0\) if the symbol and primitive recursive defining equations for predecessor :  \[ Pd(0) = 0,\]  \[ \forall x (Pd(S(x)) = x)\]  and cutoff subtraction :  \[ \forall x (x \dot{-} 0 = x),\]   \[ \forall x \forall y (x \dot{-} S(y) = Pd(x \dot{-} y))\]  are present in the formalism. \(\mathbf{HA}\) proves the comparative law