nicer proof for level13.lean

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

Apache License 2.0

288 stars 72 forks source link

Open abourque72 opened 9 months ago

abourque72 commented 9 months ago

Came up with this proof, I think it is much nicer than the one provided (which apparently was nicer than what came before it)