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

State before:
m n k : Nat
⊢ (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
Tactic:
induction m, n with
| zero_zero => rw [zero_mk_zero, Int.zero_add, Nat.zero_add]; rfl
| zero_succ n => rw [zero_mk_succ, zero_mk_succ, Nat.succ_add]; rfl
| succ_zero m => rw [succ_mk_zero, Nat.zero_add]; rfl
| succ_succ m n ih => rw [succ_mk_succ, Nat.succ_add, succ_mk_succ]; exact ih
State after:
no goals

State before:
case zero_zero
k : Nat
⊢ (0 ⊖ 0) + -[k+1] = 0 ⊖ 0 + k + 1
Tactic:
rw [zero_mk_zero, Int.zero_add, Nat.zero_add]
State after:
case zero_zero
k : Nat
⊢ -[k+1] = 0 ⊖ k + 1

State before:
case zero_zero
k : Nat
⊢ -[k+1] = 0 ⊖ k + 1
Tactic:
rfl
State after:
no goals

State before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + -[k+1] = 0 ⊖ n + k + 1
⊢ (0 ⊖ n + 1) + -[k+1] = 0 ⊖ n + 1 + k + 1
Tactic:
rw [zero_mk_succ, zero_mk_succ, Nat.succ_add]
State after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + -[k+1] = 0 ⊖ n + k + 1
⊢ -[n+1] + -[k+1] = -[(n + k).succ+1]

State before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + -[k+1] = 0 ⊖ n + k + 1
⊢ -[n+1] + -[k+1] = -[(n + k).succ+1]
Tactic:
rfl
State after:
no goals

State before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + -[k+1] = m ⊖ 0 + k + 1
⊢ (m + 1 ⊖ 0) + -[k+1] = m + 1 ⊖ 0 + k + 1
Tactic:
rw [succ_mk_zero, Nat.zero_add]
State after:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + -[k+1] = m ⊖ 0 + k + 1
⊢ ofNat (m + 1) + -[k+1] = m + 1 ⊖ k + 1

State before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + -[k+1] = m ⊖ 0 + k + 1
⊢ ofNat (m + 1) + -[k+1] = m + 1 ⊖ k + 1
Tactic:
rfl
State after:
no goals

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

State before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
⊢ (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
Tactic:
exact ih
State after:
no goals