case right =>
  intro
  have _ : succ a ≤ b := by exists w
  have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
  apply (@not_succ_le_self a)
  assumption
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ ¬b ≤ a
no goals