cases w with
| zero =>
  apply Or.inr
  exists one
  rw [add_zero] at pw
  rw [← succ_eq_add_one]
  exact succ_eq_succ_iff.mpr (Eq.symm pw)
| succ w' =>
  apply Or.inl
  exists w'
  rw [add_succ] at pw
  rw [pw, succ_add]
case succ.inl.intro
b a' w : Nat
pw : b = a' + w
⊢ succ a' ≤ b ∨ b ≤ succ a'
no goals