n m : Nat
this : n + m - m = n
⊢ n + m - m = n
n m : Nat
this : n + m - (0 + m) = n
⊢ n + m - m = n
rw [Nat.zero_add] at this
no goals
n m : Nat
this : n + m - m = n
⊢ n + m - m = n
assumption
no goals
n m : Nat
⊢ n + m - (0 + m) = n
rw [Nat.add_sub_add_right, Nat.sub_zero]