no goals
n m k : Nat
⊢ n - m - k = n - (m + k)
induction k with
| zero => simp
| succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]
no goals
case zero
n m : Nat
⊢ n - m - zero = n - (m + zero)
simp
no goals
case succ
n m k : Nat
ih : n - m - k = n - (m + k)
⊢ n - m - succ k = n - (m + succ k)
rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]