no goals
a b c : Nat
⊢ a - (b + c) = a - b - c
induction c with
| zero => simp
| succ c ih => simp [Nat.add_succ, Nat.sub_succ, ih]
no goals
case zero
a b : Nat
⊢ a - (b + zero) = a - b - zero
simp
no goals
case succ
a b c : Nat
ih : a - (b + c) = a - b - c
⊢ a - (b + succ c) = a - b - succ c
simp [Nat.add_succ, Nat.sub_succ, ih]