Theorem: LoVe.Nat.sub_one_add (LoVe/LoVelib.lean)

State before:
n m : ℕ
h : ¬n = 0
⊢ n - 1 + m = n + m - 1
Tactic:
induction n with
| zero => aesop
| succ =>
  rw [Nat.succ_add]
  aesop
State after:
no goals

State before:
case zero
m : ℕ
h : ¬Nat.zero = 0
⊢ Nat.zero - 1 + m = Nat.zero + m - 1
Tactic:
aesop
State after:
no goals

State before:
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ n_1 + m - 1
Tactic:
rw [Nat.succ_add]
State after:
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ (n_1 + m) - 1

State before:
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ (n_1 + m) - 1
Tactic:
aesop
State after:
no goals