Power World 10 uses ≠ which we don't yet know

[Ezra]

Power World 10 (Fermat's Last Theorem) is mostly pretty careful to frame it entirely in language we know: (a+1) instead of (n>0), etc. But it doesn't quite finish the job: it uses the symbol ≠, which we've never seen before unless we've digressed at least to Implication World 8. An unfamiliar symbol that we don't know how to manipulate, even a fairly common-sense one, undercuts the message that the tools we now have are enough to express big problems.

My current thought on how to improve this would be to

1. In the level explanation part of the text, mention that the symbol is new, but can for now be read in a common-sense way.
2. In the congratulations part of the text, along with the "go read Mathematics in Lean" suggestion, add an alternative of going to Implication World (if we haven't yet) to learn about ≠, and to work up to ≤ World where we'll have the full language to restate the problem more clearly.
3. (Future) If there's ever another world that depends on Power World and ≤ World, include in it a level showing how much more clearly we can now restate Fermat's Last Theorem.

Other strategies I've considered, but don't like as much, include

• Try to restate the theorem without ≠ (and without →).
• Try to explain Lean's symbol ≠ within the level text.
• Make this level depend on Implication World.

[joneugster]

I think the last option is the simplest one, i.e. add Dependency Implication → Power -- because of ≠ to the Game.lean file. @kbuzzard do you have any objection to adding this dependency to the tree?

[Tokarak]

It's not very good design if only the last level of the world depends on a previous world, especially if that level is purposefully unsolvable. Add a comment leading to Implication World instead.