Goal:
    n : t  m : t  p : t
  ============================
   (max (n + p) (m + p) = max n m + p)


DEBUG:Going to execute:
destruct n, m, p; try reflexivity