Theorem: Int.add_sub (MLIR/Util/Arith.lean)

State before:
n m : ℤ
⊢ n + (m - n) = m
Tactic:
rw [Int.sub_eq_add_neg, Int.add_comm m (-n), ←Int.add_assoc,
    Int.add_right_neg, Int.zero_add]
State after:
no goals