Theorem: LoVe.Nat.add_sub_again (LoVe/LoVelib.lean)

State before:
m n : ℕ
⊢ m + n - m = n
Tactic:
induction m with
| zero => simp
| succ m' ih => rw [Nat.succ_add, Nat.succ_sub_succ, ih]
State after:
no goals

State before:
case zero
n : ℕ
⊢ Nat.zero + n - Nat.zero = n
Tactic:
simp
State after:
no goals

State before:
case succ
n m' : ℕ
ih : m' + n - m' = n
⊢ Nat.succ m' + n - Nat.succ m' = n
Tactic:
rw [Nat.succ_add, Nat.succ_sub_succ, ih]
State after:
no goals