>>>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!!