Stuck on Natural Number Game Advanced Addition 5

Stream: new members

[John Smith]

Hello! Im new here so I apologise if this isn't the correct place to ask, but im completely stuck on this level. Ive tried this, and some similar ideas, but I really have no clue how else to proceed and id appreciate any advice. Thanks!
Screenshot 2025-10-01 at 20.24.26.png

[John Smith]

I think its a type error since (a+d) is an addition and it wants to take in a natural number, but (a+d) is of course still just a natural and Im not sure how to rectify that, is there so way I can rewrite it as some other natural n?

[Ilmārs Cīrulis]

I believe you need to use symm on the h and only then the apply.

[John Smith]

I had tried that and it didn't seem like anything happened but it could just be a terrible wifi issue, ill give it another go

[Ilmārs Cīrulis]

If the symm works as I imagine there, then after using it the hypothesis will be in correct form for the apply zero_ne_succ at h.

[Anthony Wang]

The symm is unnecessary since you can directly do apply succ_ne_zero at h (not zero_ne_succ)

[John Smith]

I don't have succ_ne_zero yet and symm doesn't appear to be doing anything. Somewhat confused

[Ilmārs Cīrulis]

Works for me... :thinking:

image.png

[John Smith]

It seems to accept the command but then nothing happens...
Screenshot 2025-10-01 at 20.44.27.png

[Ilmārs Cīrulis]

Can you try the Retry button?

[John Smith]

Yeah, ive tried that a few times now and nothing seems to happen, very odd

[John Smith]

Ill possibly try writing everything out in the editor mode and see if its any happier with that

[John Smith]

That seems to work, im not exactly sure why that makes a difference but ill take the win

[Kevin Buzzard]

PS

John Smith said:

Hello! Im new here so I apologise if this isn't the correct place to ask, but im completely stuck on this level. Ive tried this, and some similar ideas, but I really have no clue how else to proceed and id appreciate any advice. Thanks!

Here is precisely the correct place to ask, although we prefer real names.