have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
a b : Nat
x✝¹ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝ : succ a ≤ b
⊢ False
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ False