Help Needed on Natural Number Game 6/8 LessOrEqual

Stream: new members

[Qi Wen Wei]

Hi! I'm a beginner trying to go through the Natural Number Game but I've gotten stuck on this level: https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/LessOrEqual/level/6.

My current feeling is that it has something to do with induction but I can't seem to figure it out. Is anyone able to provide a hint? I would appreciate it very much. :pray:

[chenjulang]

Try this:
https://github.com/adyavanapalli/natural-number-game-solutions

[Qi Wen Wei]

I think those are the solutions to the old natural number game (lean 3). Are there any solutions to the new version?

[chenjulang]

Just search the answer from the repository itself. :grinning_face_with_smiling_eyes:
https://github.com/leanprover-community/NNG4/tree/26a39e345915526865467053efbe6f0380eeb6cd

[Qi Wen Wei]

chenjulang said:

Just search the answer from the repository itself. :grinning_face_with_smiling_eyes:
https://github.com/leanprover-community/NNG4/tree/26a39e345915526865467053efbe6f0380eeb6cd

Oh Damn, I didn't think of that. Thanks for the help!

[chenjulang]

It is easy to create your own game too, try it.

[Kevin Buzzard]

The hint is "remove all <= and reduce to a problem which we solved already"