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

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.

• Hint 1: Note that in the natural numbers, succ d can never be 0. So your mistake has to be before you got to the goal succ d = 0. Hint 2: Have you tried it on paper? Oct 30, 2023 at 1:32

this is my proof that uses the rules of the game

cases hx
contrapose! h
symm
intro t

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