Theorem: Int.sub_add_assoc (Extra/Int/Lemmas.lean)

State before:
i j k : Int
⊢ i - j + k = i + -j + k
Tactic:
rw [Int.sub_eq]
State after:
no goals

State before:
i j k : Int
⊢ i + -j + k = i + (-j + k)
Tactic:
rw [Int.add_assoc]
State after:
no goals

State before:
i j k : Int
⊢ i + (-j + k) = i + (-j + - -k)
Tactic:
rw [Int.neg_neg]
State after:
no goals

State before:
i j k : Int
⊢ i + (-j + - -k) = i + -(j + -k)
Tactic:
rw [Int.neg_add]
State after:
no goals

State before:
i j k : Int
⊢ i + -(j + -k) = i - (j - k)
Tactic:
rw [Int.sub_eq, Int.sub_eq]
State after:
no goals