intro
| ⟨w , pw⟩  =>
  constructor
  case left =>
    exists (w + one)
    rw [pw, succ_eq_add_one]
    simp
  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
⊢ succ a ≤ b → a ≤ b ∧ ¬b ≤ a
no goals