Theorem: Int.add_sub_cancel_right (Util/Arithmetic.lean)

State before:
a✝ b✝ : ℕ
a b c : ℤ
⊢ a + (b - a) = b
Tactic:
rewrite [Int.add_comm]
State after:
a✝ b✝ : ℕ
a b c : ℤ
⊢ b - a + a = b

State before:
a✝ b✝ : ℕ
a b c : ℤ
⊢ b - a + a = b
Tactic:
apply Int.sub_add_cancel
State after:
no goals