EDB — 28C

[28C] If $m\ge n$, there exists an unique $h$ such that $m=n+h$ (uniqueness follows from [27V]↺↻); we will indicate this $h$ as $m-n$.