cases ih with
| inl h =>
  cases h with
  | intro w pw =>
    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]
| inr h =>
  apply Or.inr
  apply le_succ
  assumption
case succ
b a' : Nat
ih : a' ≤ b ∨ b ≤ a'
⊢ succ a' ≤ b ∨ b ≤ succ a'
no goals