>>>14420889to the anon working through the Natural Numbers game:
I'm going to give you a small hint on how to get each of the goals you get after applying
[code:lit]
induction c with d hd generalizing b,
[code:lit]
(idk if these clues will work if you did it with the first suggested method)
goal 1) apply
[code:lit]
by_cases bb : b = 0,
[code:lit]
this splits the goal into two more goals:
* easy
* what theorem statement relates a=/=0, b=/0 and a*b=/=0?
goal 2) similarly, apply
[code:lit]
cases b,
[code:lit]
this splits the goal into two more goals:
* can you see a contradiction in one of your assumptions?
if one of your assumptions is of the form c*d=0, what theorem statement can break this up into (c=0 OR d=0)?
what can you do to make one of these an assumption and eliminate the OR statement?
* easy
please post your progress or the closest you think you've gotten!!
