cases w with
| zero =>
  rw [add_zero] at pw
  have _ : b ≤ a := pw ▸ (le_refl b)  contradiction
| succ w' =>
  exists w'
  rw [pw, add_succ, succ_add]
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
w : Nat
pw : b = a + w
hc : ¬b ≤ a
⊢ succ a ≤ b
no goals