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]
case succ.inl
b a' : Nat
h : a' ≤ b
⊢ succ a' ≤ b ∨ b ≤ succ a'
no goals