0 [`m < n`]
  1 [`?d. n = m + SUC d`]
  2 [`n = m + SUC d`]
  3 [`n = m + d + 1`]
  4 [`n = (m + d) + 1`]
  5 [`n = 1 + m + d`]

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