0 [`m < n`]
  1 [`?d. n = m + SUC d`]
  2 [`n = m + SUC d`]

`m <= n - 1`
--------------------------------------------------------------------------------
1/1 (1)