Zulip Chat Archive

Stream: new members

Topic: Natural Numbers Game Advanced Multiplication


Amya (Aug 19 2024 at 02:53):

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 (Aug 19 2024 at 03:49):

Have you tried cases ha with b hb?

Amya (Aug 19 2024 at 13:02):

That worked! Thank you!!


Last updated: May 02 2025 at 03:31 UTC