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