Even/odd world
Opened this issue · 2 comments
We need an even/odd world. A proposal: IsEven x := \exists t, x = t + t, IsOdd x := \exists t, x = t + t + 1, and then the boss levels of that world is that every natural is either even or odd, and that no natural is both even and odd.
Ivan has started on writing the Lean code (but I don't have a link).
My code is here https://github.com/ifarabella/NNG4 . The relevant theorems are under NNG4/Game/Levels/EvenOddTest
Ivan I cleaned up your code and put it here. Right now the plan is to have even-odd world after advanced addition world, which will introduce the theorems succ_inj and succ_ne_zero, and the tactics intro, exact and apply (and apply ... at). I want even-odd world to teach use and rcases. What we really need is ten or so files each containing one theorem from the levels of even-odd world, like we have already with addition world etc.