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?