Theorem: Nat.sub_add_eq_add_sub (QuickSortInLean/QuickSort.lean)

State before:
m n k : Nat
km : k ≤ m
⊢ m - k + n = m + n - k
Tactic:
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]
State after:
no goals

State before:
case refl
m n k : Nat
⊢ k - k + n = k + n - k
Tactic:
simp [Nat.add_sub_cancel_left]
State after:
no goals

State before:
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
Tactic:
have : k ≤ m + n := Nat.le_trans km (Nat.le_add_right ..)
State after:
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

State before:
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
Tactic:
simp [Nat.succ_sub km, Nat.succ_add, ih, Nat.succ_sub this]
State after:
no goals