have : k ≤ m + n := Nat.le_trans km (Nat.le_add_right ..)
case step
m✝ n k m : Nat
km : k.le m
ih : m - k + n = m + n - k
⊢ m.succ - k + n = m.succ + n - k
case step
m✝ n k m : Nat
km : k.le m
ih : m - k + n = m + n - k
this : k ≤ m + n
⊢ m.succ - k + n = m.succ + n - k