Lambda Calculus Prove Equality Excessive (Haskell-oriented)
Another way is to continue from where you got stuck, in the inductive step. You have:
$(Sx+n)−Sx=S(x+n)−Sx$

Now you can prove the following lemma by induction on y:


  Lemma:  $Sx - Sy = x - y$
  
  
  case 0:     $S(x) - S(0) = pred (S(x) - 0) = pred(S(x)) = x = x - 0$
  given $Sx - Sy = x - y$, case $Sy$
  
  $Sx - S(Sy) = pred (Sx - Sy) = pred (x - y) = x - Sy$
  


then you continue:

$(Sx+n)−Sx=S(x+n)−Sx =^{(lemma)} (x + n) - x =^{(IH)} n $