Natural Numbers Game Advanced Multiplication

Stream: new members

[Amya]

I am stuck on Advanced Multiplication World Level 4, which asks me to prove that if a natural number 𝑎≠0, then 𝑎≥1. The tutorial called this proof 'one_le_of_ne_zero.'

There's what I have so far:

apply eq_succ_of_ne_zero at ha
rw [one_eq_succ_zero]

This turns the hypothesis into $\exists n, a = succ n$ and the goal into $succ 0 \leq a$. I know that I need to use the hypothesis to substitute 𝑎 with 𝑠𝑢𝑐𝑐 𝑛, followed by apply succ_le_succ and apply zero_le. But I can't figure out what is the code to use the hypothesis and make this substitution. Can anyone help me?

[Bulhwi Cha]

Have you tried cases ha with b hb?

[Amya]

That worked! Thank you!!