intro
| Or.inl h => exact Nat.le_of_succ_le_succ h
| Or.inr h => absurd h; apply Nat.succ_ne_zero
case succ_succ.mp
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0 → x + 1 ≤ y + 1 - 1
no goals