le_succ_self

Stream: new members

[Alan Post]

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=10&level=10
In Inequality World, level 10, le_succ_self, the description says "Can you find the two-line proof?"

I was surprised by this, because while I've found the Natural Number Game quite challenging in general, I thought the one-line proof "exact le_succ a a (le_refl a)," was the obvious way to go for this one.

[Ruben Van de Velde]

That's a good proof, indeed. Perhaps it means "the two-line proof without using earlier lemmas"

[Eric Wieser]

Looking at the answers, that is indeed what it means

[Alan Post]

(deleted)

[Kevin Buzzard]

It's always nice to be golfed :-) You should open an issue saying you found a 1 line proof and want your money back :-)

[Alan Post]

I'm very appreciative of the Natural Number Game, and will happily pay full price for any sequels. :grinning: