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

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