no goals
n k m : ℕ
⊢ n + k - (m + k) + (m + k - (n + k)) = n - m + (m + k - (n + k))
rw [@add_tsub_add_eq_tsub_right]
no goals
n k m : ℕ
⊢ n - m + (m + k - (n + k)) = n - m + (m - n)
rw [@add_tsub_add_eq_tsub_right]