How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?

Question

I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, then x must be 0. The formal statement is ∀ (x : ℕ), x ≤ 0 → x = 0.

Here's my current code:

theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by {
  apply le_trans x 0 x at hx,
  cases x with d,
  rfl,
  symm,
  -- Now I have a goal of `succ d = 0`
  apply zero_le at hx,
  -- Stuck here, it says 'oops'
}

I applied le_trans and then used cases to handle the base case x = 0 and the successor case x = succ d. The base case is easily solved with rfl, but I'm stuck on the successor case.

Answer 1

this is my proof that uses the rules of the game

cases hx
contrapose! h
symm
intro t
apply eq_zero_of_add_right_eq_zero at t
apply h at t
exact t

Not sure if cases is allowed at the beginning without a with but it seems to be accepted, Game will accept this proof.

---

Edit: Someone posted another shorter proof, but I don't see their proof anymore, so here it goes

cases hx with a ha
exact eq_zero_of_add_right_eq_zero _ _ ha.symm