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

State before:
k m n : Nat
⊢ m + k ⊖ n + k = m ⊖ n
Tactic:
induction k with
| zero => rw [Nat.add_zero, Nat.add_zero]
| succ k ih => rw [Nat.add_succ m k, Nat.add_succ n k, succ_mk_succ]; exact ih
State after:
no goals

State before:
case zero
m n : Nat
⊢ m + 0 ⊖ n + 0 = m ⊖ n
Tactic:
rw [Nat.add_zero, Nat.add_zero]
State after:
no goals

State before:
case succ
m n k : Nat
ih : m + k ⊖ n + k = m ⊖ n
⊢ m + (k + 1) ⊖ n + (k + 1) = m ⊖ n
Tactic:
rw [Nat.add_succ m k, Nat.add_succ n k, succ_mk_succ]
State after:
case succ
m n k : Nat
ih : m + k ⊖ n + k = m ⊖ n
⊢ m + k ⊖ n + k = m ⊖ n

State before:
case succ
m n k : Nat
ih : m + k ⊖ n + k = m ⊖ n
⊢ m + k ⊖ n + k = m ⊖ n
Tactic:
exact ih
State after:
no goals