Goal:
    n : t  m : t  p : t  q : t
  ============================
   (n <= m -> p <= q -> n + p <= m + q)


DEBUG:Going to execute:
destruct n, m, p, q; cbn