no goals
a b : Nat
h : a ≤ b
⊢ a + (b - a) = b
induction a with
| zero => simp
| succ a ih =>
  have hne : b - a ≠ 0 := Nat.sub_ne_zero_of_lt h
  have : a ≤ b := Nat.le_of_succ_le h
  rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this]
no goals
case zero
b : Nat
h : zero ≤ b
⊢ zero + (b - zero) = b
simp
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : succ a ≤ b
hne : b - a ≠ 0
⊢ succ a + (b - succ a) = b
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : succ a ≤ b
⊢ succ a + (b - succ a) = b
have hne : b - a ≠ 0 := Nat.sub_ne_zero_of_lt h
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : succ a ≤ b
hne : b - a ≠ 0
this : a ≤ b
⊢ succ a + (b - succ a) = b
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : succ a ≤ b
hne : b - a ≠ 0
⊢ succ a + (b - succ a) = b
have : a ≤ b := Nat.le_of_succ_le h
no goals
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : succ a ≤ b
hne : b - a ≠ 0
this : a ≤ b
⊢ succ a + (b - succ a) = b
rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this]