Goal:
    n : Z  m : t
  ============================
   ((0 <= n)%Z -> m <= Some n + m)


DEBUG:Going to execute:
destruct m; cbn