Lambda Calculus Prove Equality Excessive (Haskell-oriented) I'm on a lambda calculus with parametric polymorphism a la Hindley-Milner Haskell-oriented course and I'm currently facing this exercise which I got stuck on.

Prove that $(\forall m\downarrow, n\downarrow :: N)\space (m+n)-m=n$

Definitions:

$(+)=\backslash m \space n \rightarrow case \space m \space of \space \{0\rightarrow n, Sx \rightarrow S(x+n)\}$

$pred = \backslash n \rightarrow case \space n \space of\{0\rightarrow 0,Sx\rightarrow x\}$

$(-)= \backslash m \space n \rightarrow case \space n \space of \space \{0\rightarrow m,Sx\rightarrow pred(m-x)\}$

Seems super simple but there's a part at which I got stuck. I also can only use the following already proven statements (may not need all):

$1) \space m+0=m$

$2) \space m + Sx = S(m+x)$

$3) \space m+n=n+m$

So here's what I did so far: I decided to prove this by using induction over m

$m=0, \space (0+n)-0=n-0=n$ is true (applying the given definitions for the functions)

$m=x, \space (m+n)-m=n$ is true (Hypothesis)

$m=Sx, \space (Sx+n)-Sx=n$ is true (Thesis)

Proof for $m=Sx$:

$(Sx+n)-Sx=S(x+n)-Sx=pred(S(x+n)-x)$ At which point I got stuck. I obviously have to get that $S$ out of $S(x+n)-n$ to have $(x+n)-n$ and apply the Hypothesis but I can't figure out how. Any ideas?
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 $