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