induction km with
| refl => simp [Nat.add_sub_cancel_left]
| @step m km ih =>
  have : k ≤ m + n := Nat.le_trans km (Nat.le_add_right ..)
  simp [Nat.succ_sub km, Nat.succ_add, ih, Nat.succ_sub this]
m n k : Nat
km : k ≤ m
⊢ m - k + n = m + n - k
no goals