induction a with
| zero => apply Or.inl; exact (zero_le _)
| succ a' ih =>
  cases ih with
  | inl h =>
    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]
  | inr h =>
    apply Or.inr
    apply le_succ
    assumption
a b : Nat
⊢ a ≤ b ∨ b ≤ a
no goals