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

State before:
m : Nat
⊢ m ⊖ m = 0
Tactic:
induction m with
| zero => rfl
| succ m ih => rw [succ_mk_succ]; exact ih
State after:
no goals

State before:
case zero

⊢ 0 ⊖ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
m : Nat
ih : m ⊖ m = 0
⊢ m + 1 ⊖ m + 1 = 0
Tactic:
rw [succ_mk_succ]
State after:
case succ
m : Nat
ih : m ⊖ m = 0
⊢ m ⊖ m = 0

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