cases h with
| intro w pw =>
  rw [succ_eq_add_one, add_comm_right, add_assoc] at pw
  have hw : w + one = zero := eq_zero_of_add_right_eq_self (Eq.symm pw)
  have _ : one = zero := add_left_eq_zero hw
  contradiction
a : Nat
h : succ a ≤ a
⊢ False
no goals