no goals
n : Nat
⊢ 0 - n = 0
induction n with
| zero => rfl
| succ n ih => simp [ih, Nat.sub_succ]
no goals
case zero

⊢ 0 - zero = 0
rfl
no goals
case succ
n : Nat
ih : 0 - n = 0
⊢ 0 - succ n = 0
simp [ih, Nat.sub_succ]